Theorem ocasepS | index | src |

theorem ocasepS (S: set) (n: nat) (z: wff): $ suc n e. ocasep z S <-> n e. S $;
StepHypRefExpression
1 eleq1
suc n - 1 = n -> (suc n - 1 e. S <-> n e. S)
2 sucsub1
suc n - 1 = n
3 1, 2 ax_mp
suc n - 1 e. S <-> n e. S
4 ifpneg
~suc n = 0 -> (ifp (suc n = 0) z (suc n - 1 e. S) <-> suc n - 1 e. S)
5 peano1
suc n != 0
6 5 conv ne
~suc n = 0
7 4, 6 ax_mp
ifp (suc n = 0) z (suc n - 1 e. S) <-> suc n - 1 e. S
8 eqeq1
a1 = suc n -> (a1 = 0 <-> suc n = 0)
9 biidd
a1 = suc n -> (z <-> z)
10 subeq1
a1 = suc n -> a1 - 1 = suc n - 1
11 10 eleq1d
a1 = suc n -> (a1 - 1 e. S <-> suc n - 1 e. S)
12 8, 9, 11 ifpeqd
a1 = suc n -> (ifp (a1 = 0) z (a1 - 1 e. S) <-> ifp (suc n = 0) z (suc n - 1 e. S))
13 7, 12 syl6bb
a1 = suc n -> (ifp (a1 = 0) z (a1 - 1 e. S) <-> suc n - 1 e. S)
14 3, 13 syl6bb
a1 = suc n -> (ifp (a1 = 0) z (a1 - 1 e. S) <-> n e. S)
15 14 elabe
suc n e. {a1 | ifp (a1 = 0) z (a1 - 1 e. S)} <-> n e. S
16 15 conv ocasep
suc n e. ocasep z S <-> n e. 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)