Theorem obindeqS ≪ | index | src | ≫ 

theorem obindeqS (F: set) (a: nat) {m: nat} (n: nat):
  $ obind n F = suc a <-> E. m (n = suc m /\ F @ m = suc a) $;
StepHypRefExpression
1 sucne0 
obind n F = suc a -> obind n F != 0
2 absurdr 
obind n F = 0 -> ~obind n F = 0 -> E. m (n = suc m /\ F @ m = suc a)
3 2 conv ne 
obind n F = 0 -> obind n F != 0 -> E. m (n = suc m /\ F @ m = suc a)
4 obind0 
obind 0 F = 0
5 obindeq1 
n = 0 -> obind n F = obind 0 F
6 4, 5 syl6eq 
n = 0 -> obind n F = 0
7 3, 6 syl 
n = 0 -> obind n F != 0 -> E. m (n = suc m /\ F @ m = suc a)
8 1, 7 syl5 
n = 0 -> obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
9 exsuc 
n != 0 <-> E. m n = suc m
10 9 conv ne 
~n = 0 <-> E. m n = suc m
11 anr 
obind n F = suc a /\ n = suc m -> n = suc m
12 obindS 
obind (suc m) F = F @ m
13 11 obindeq1d 
obind n F = suc a /\ n = suc m -> obind n F = obind (suc m) F
14 12, 13 syl6eq 
obind n F = suc a /\ n = suc m -> obind n F = F @ m
15 anl 
obind n F = suc a /\ n = suc m -> obind n F = suc a
16 14, 15 eqtr3d 
obind n F = suc a /\ n = suc m -> F @ m = suc a
17 11, 16 iand 
obind n F = suc a /\ n = suc m -> n = suc m /\ F @ m = suc a
18 17 exp 
obind n F = suc a -> n = suc m -> n = suc m /\ F @ m = suc a
19 18 eximd 
obind n F = suc a -> E. m n = suc m -> E. m (n = suc m /\ F @ m = suc a)
20 19 com12 
E. m n = suc m -> obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
21 10, 20 sylbi 
~n = 0 -> obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
22 8, 21 cases 
obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
23 obindeq1 
n = suc m -> obind n F = obind (suc m) F
24 12, 23 syl6eq 
n = suc m -> obind n F = F @ m
25 24 anwl 
n = suc m /\ F @ m = suc a -> obind n F = F @ m
26 anr 
n = suc m /\ F @ m = suc a -> F @ m = suc a
27 25, 26 eqtrd 
n = suc m /\ F @ m = suc a -> obind n F = suc a
28 27 eex 
E. m (n = suc m /\ F @ m = suc a) -> obind n F = suc a
29 22, 28 ibii 
obind n F = suc a <-> E. m (n = suc m /\ F @ m = suc 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)