Theorem ocasep_Tail ≪ | index | src | ≫ 

theorem ocasep_Tail (S: set): $ ocasep (0 e. S) (Tail S) == S $;
StepHypRefExpression
1 ocasep0 
0 e. ocasep (0 e. S) (Tail S) <-> 0 e. S
2 eleq1 
a1 = 0 -> (a1 e. ocasep (0 e. S) (Tail S) <-> 0 e. ocasep (0 e. S) (Tail S))
3 eleq1 
a1 = 0 -> (a1 e. S <-> 0 e. S)
4 2, 3 bieqd 
a1 = 0 -> (a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S <-> (0 e. ocasep (0 e. S) (Tail S) <-> 0 e. S))
5 1, 4 mpbiri 
a1 = 0 -> (a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S)
6 exsuc 
a1 != 0 <-> E. a2 a1 = suc a2
7 6 conv ne 
~a1 = 0 <-> E. a2 a1 = suc a2
8 bitr 
(suc a2 e. ocasep (0 e. S) (Tail S) <-> a2 e. Tail S) -> (a2 e. Tail S <-> suc a2 e. S) -> (suc a2 e. ocasep (0 e. S) (Tail S) <-> suc a2 e. S)
9 ocasepS 
suc a2 e. ocasep (0 e. S) (Tail S) <-> a2 e. Tail S
10 8, 9 ax_mp 
(a2 e. Tail S <-> suc a2 e. S) -> (suc a2 e. ocasep (0 e. S) (Tail S) <-> suc a2 e. S)
11 elTail 
a2 e. Tail S <-> suc a2 e. S
12 10, 11 ax_mp 
suc a2 e. ocasep (0 e. S) (Tail S) <-> suc a2 e. S
13 eleq1 
a1 = suc a2 -> (a1 e. ocasep (0 e. S) (Tail S) <-> suc a2 e. ocasep (0 e. S) (Tail S))
14 eleq1 
a1 = suc a2 -> (a1 e. S <-> suc a2 e. S)
15 13, 14 bieqd 
a1 = suc a2 -> (a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S <-> (suc a2 e. ocasep (0 e. S) (Tail S) <-> suc a2 e. S))
16 12, 15 mpbiri 
a1 = suc a2 -> (a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S)
17 16 eex 
E. a2 a1 = suc a2 -> (a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S)
18 7, 17 sylbi 
~a1 = 0 -> (a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S)
19 5, 18 cases 
a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S
20 19 ax_gen 
A. a1 (a1 e. ocasep (0 e. S) (Tail S) <-> a1 e. S)
21 20 conv eqs 
ocasep (0 e. S) (Tail S) == S

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, add0, addS)