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
 
obind n F = suc a -> obind n F != 0
2
 
obind n F = 0 -> ~obind n F = 0 -> E. m (n = suc m /\ F @ m = suc a)
3
conv ne
 
obind n F = 0 -> obind n F != 0 -> E. m (n = suc m /\ F @ m = suc a)
4
 
obind 0 F = 0
5
 
n = 0 -> obind n F = obind 0 F
6
4, 5
 
n = 0 -> obind n F = 0
7
3, 6
 
n = 0 -> obind n F != 0 -> E. m (n = suc m /\ F @ m = suc a)
8
1, 7
 
n = 0 -> obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
9
 
n != 0 <-> E. m n = suc m
10
conv ne
 
~n = 0 <-> E. m n = suc m
11
 
obind n F = suc a /\ n = suc m -> n = suc m
12
 
obind (suc m) F = F @ m
13
 
obind n F = suc a /\ n = suc m -> obind n F = obind (suc m) F
14
 
obind n F = suc a /\ n = suc m -> obind n F = F @ m
15
 
obind n F = suc a /\ n = suc m -> obind n F = suc a
16
 
obind n F = suc a /\ n = suc m -> F @ m = suc a
17
 
obind n F = suc a /\ n = suc m -> n = suc m /\ F @ m = suc a
18
 
obind n F = suc a -> n = suc m -> n = suc m /\ F @ m = suc a
19
 
obind n F = suc a -> E. m n = suc m -> E. m (n = suc m /\ F @ m = suc a)
20
 
E. m n = suc m -> obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
21
 
~n = 0 -> obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
22
8, 21
 
obind n F = suc a -> E. m (n = suc m /\ F @ m = suc a)
23
 
n = suc m -> obind n F = obind (suc m) F
24
 
n = suc m -> obind n F = F @ m
25
 
n = suc m /\ F @ m = suc a -> obind n F = F @ m
26
 
n = suc m /\ F @ m = suc a -> F @ m = suc a
27
 
n = suc m /\ F @ m = suc a -> obind n F = suc a
28
 
E. m (n = suc m /\ F @ m = suc a) -> obind n F = suc a
29
 
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)