Theorem FstSnd ≪ | index | src | ≫ 

theorem FstSnd (A: set): $ Sum (Fst A) (Snd A) == A $;
StepHypRefExpression
1 eor 
(a1 = b0 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)) ->
  (a1 = b1 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)) ->
  a1 = b0 (a1 // 2) \/ a1 = b1 (a1 // 2) ->
  (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)
2 bitr 
(b0 (a1 // 2) e. Sum (Fst A) (Snd A) <-> a1 // 2 e. Fst A) ->
  (a1 // 2 e. Fst A <-> b0 (a1 // 2) e. A) ->
  (b0 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b0 (a1 // 2) e. A)
3 Suml 
b0 (a1 // 2) e. Sum (Fst A) (Snd A) <-> a1 // 2 e. Fst A
4 2, 3 ax_mp 
(a1 // 2 e. Fst A <-> b0 (a1 // 2) e. A) -> (b0 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b0 (a1 // 2) e. A)
5 elFst 
a1 // 2 e. Fst A <-> b0 (a1 // 2) e. A
6 4, 5 ax_mp 
b0 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b0 (a1 // 2) e. A
7 eleq1 
a1 = b0 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> b0 (a1 // 2) e. Sum (Fst A) (Snd A))
8 eleq1 
a1 = b0 (a1 // 2) -> (a1 e. A <-> b0 (a1 // 2) e. A)
9 7, 8 bieqd 
a1 = b0 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A <-> (b0 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b0 (a1 // 2) e. A))
10 6, 9 mpbiri 
a1 = b0 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)
11 1, 10 ax_mp 
(a1 = b1 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)) -> a1 = b0 (a1 // 2) \/ a1 = b1 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)
12 bitr 
(b1 (a1 // 2) e. Sum (Fst A) (Snd A) <-> a1 // 2 e. Snd A) ->
  (a1 // 2 e. Snd A <-> b1 (a1 // 2) e. A) ->
  (b1 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b1 (a1 // 2) e. A)
13 Sumr 
b1 (a1 // 2) e. Sum (Fst A) (Snd A) <-> a1 // 2 e. Snd A
14 12, 13 ax_mp 
(a1 // 2 e. Snd A <-> b1 (a1 // 2) e. A) -> (b1 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b1 (a1 // 2) e. A)
15 elSnd 
a1 // 2 e. Snd A <-> b1 (a1 // 2) e. A
16 14, 15 ax_mp 
b1 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b1 (a1 // 2) e. A
17 eleq1 
a1 = b1 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> b1 (a1 // 2) e. Sum (Fst A) (Snd A))
18 eleq1 
a1 = b1 (a1 // 2) -> (a1 e. A <-> b1 (a1 // 2) e. A)
19 17, 18 bieqd 
a1 = b1 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A <-> (b1 (a1 // 2) e. Sum (Fst A) (Snd A) <-> b1 (a1 // 2) e. A))
20 16, 19 mpbiri 
a1 = b1 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)
21 11, 20 ax_mp 
a1 = b0 (a1 // 2) \/ a1 = b1 (a1 // 2) -> (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)
22 b0orb1 
a1 = b0 (a1 // 2) \/ a1 = b1 (a1 // 2)
23 21, 22 ax_mp 
a1 e. Sum (Fst A) (Snd A) <-> a1 e. A
24 23 ax_gen 
A. a1 (a1 e. Sum (Fst A) (Snd A) <-> a1 e. A)
25 24 conv eqs 
Sum (Fst A) (Snd A) == A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)