Theorem theo01 ≪ | index | src | ≫ 

theorem theo01 {y x: nat} (A: set): $ ~E. y A == {x | x = y} -> theo A = 0 $;
StepHypRefExpression
1 the0 
~E. n {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n} -> the {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} = 0
2 1 conv theo 
~E. n {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n} -> theo A = 0
3 con3 
(E. n {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n} -> E. y A == {x | x = y}) ->
  ~E. y A == {x | x = y} ->
  ~E. n {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n}
4 bitr 
(A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a3 | a3 = n}) ->
  ({a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a3 | a3 = n} <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n}) ->
  (A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n})
5 abeqb 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a3 | a3 = n}
6 4, 5 ax_mp 
({a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a3 | a3 = n} <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n}) ->
  (A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n})
7 eqseq2 
{a3 | a3 = n} == {a1 | a1 = n} -> ({a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a3 | a3 = n} <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n})
8 eqeq1 
a3 = a1 -> (a3 = n <-> a1 = n)
9 8 cbvab 
{a3 | a3 = n} == {a1 | a1 = n}
10 7, 9 ax_mp 
{a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a3 | a3 = n} <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n}
11 6, 10 ax_mp 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) <-> {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n}
12 eqeq1 
a3 = n -> (a3 = suc a2 <-> n = suc a2)
13 12 aneq1d 
a3 = n -> (a3 = suc a2 /\ a2 e. A <-> n = suc a2 /\ a2 e. A)
14 13 exeqd 
a3 = n -> (E. a2 (a3 = suc a2 /\ a2 e. A) <-> E. a2 (n = suc a2 /\ a2 e. A))
15 eqeq1 
a3 = n -> (a3 = n <-> n = n)
16 14, 15 bieqd 
a3 = n -> (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n <-> (E. a2 (n = suc a2 /\ a2 e. A) <-> n = n))
17 16 eale 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> (E. a2 (n = suc a2 /\ a2 e. A) <-> n = n)
18 suceq 
y = a2 -> suc y = suc a2
19 18 eqeq2d 
y = a2 -> (n = suc y <-> n = suc a2)
20 eleq1 
y = a2 -> (y e. A <-> a2 e. A)
21 19, 20 aneqd 
y = a2 -> (n = suc y /\ y e. A <-> n = suc a2 /\ a2 e. A)
22 21 cbvex 
E. y (n = suc y /\ y e. A) <-> E. a2 (n = suc a2 /\ a2 e. A)
23 eqid 
n = n
24 bi2 
(E. a2 (n = suc a2 /\ a2 e. A) <-> n = n) -> n = n -> E. a2 (n = suc a2 /\ a2 e. A)
25 23, 24 mpi 
(E. a2 (n = suc a2 /\ a2 e. A) <-> n = n) -> E. a2 (n = suc a2 /\ a2 e. A)
26 22, 25 sylibr 
(E. a2 (n = suc a2 /\ a2 e. A) <-> n = n) -> E. y (n = suc y /\ y e. A)
27 17, 26 rsyl 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> E. y (n = suc y /\ y e. A)
28 peano2 
suc x = suc y <-> x = y
29 eleq1 
a2 = x -> (a2 e. A <-> x e. A)
30 suceq 
a2 = x -> suc a2 = suc x
31 30 eqeq1d 
a2 = x -> (suc a2 = n <-> suc x = n)
32 29, 31 imeqd 
a2 = x -> (a2 e. A -> suc a2 = n <-> x e. A -> suc x = n)
33 32 eale 
A. a2 (a2 e. A -> suc a2 = n) -> x e. A -> suc x = n
34 eexb 
E. a2 (a3 = suc a2 /\ a2 e. A) -> a3 = n <-> A. a2 (a3 = suc a2 /\ a2 e. A -> a3 = n)
35 bi1 
(E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> E. a2 (a3 = suc a2 /\ a2 e. A) -> a3 = n
36 34, 35 sylib 
(E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> A. a2 (a3 = suc a2 /\ a2 e. A -> a3 = n)
37 36 alimi 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> A. a3 A. a2 (a3 = suc a2 /\ a2 e. A -> a3 = n)
38 ax_11 
A. a3 A. a2 (a3 = suc a2 /\ a2 e. A -> a3 = n) -> A. a2 A. a3 (a3 = suc a2 /\ a2 e. A -> a3 = n)
39 ian 
suc a2 = suc a2 -> a2 e. A -> suc a2 = suc a2 /\ a2 e. A
40 eqid 
suc a2 = suc a2
41 39, 40 ax_mp 
a2 e. A -> suc a2 = suc a2 /\ a2 e. A
42 41 imim1i 
(suc a2 = suc a2 /\ a2 e. A -> suc a2 = n) -> a2 e. A -> suc a2 = n
43 eqeq1 
a3 = suc a2 -> (a3 = suc a2 <-> suc a2 = suc a2)
44 43 aneq1d 
a3 = suc a2 -> (a3 = suc a2 /\ a2 e. A <-> suc a2 = suc a2 /\ a2 e. A)
45 eqeq1 
a3 = suc a2 -> (a3 = n <-> suc a2 = n)
46 44, 45 imeqd 
a3 = suc a2 -> (a3 = suc a2 /\ a2 e. A -> a3 = n <-> suc a2 = suc a2 /\ a2 e. A -> suc a2 = n)
47 46 eale 
A. a3 (a3 = suc a2 /\ a2 e. A -> a3 = n) -> suc a2 = suc a2 /\ a2 e. A -> suc a2 = n
48 42, 47 syl 
A. a3 (a3 = suc a2 /\ a2 e. A -> a3 = n) -> a2 e. A -> suc a2 = n
49 48 alimi 
A. a2 A. a3 (a3 = suc a2 /\ a2 e. A -> a3 = n) -> A. a2 (a2 e. A -> suc a2 = n)
50 38, 49 rsyl 
A. a3 A. a2 (a3 = suc a2 /\ a2 e. A -> a3 = n) -> A. a2 (a2 e. A -> suc a2 = n)
51 37, 50 rsyl 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> A. a2 (a2 e. A -> suc a2 = n)
52 51 anwll 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x e. A -> A. a2 (a2 e. A -> suc a2 = n)
53 anr 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x e. A -> x e. A
54 33, 52, 53 sylc 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x e. A -> suc x = n
55 eleq1 
a2 = y -> (a2 e. A <-> y e. A)
56 suceq 
a2 = y -> suc a2 = suc y
57 56 eqeq1d 
a2 = y -> (suc a2 = n <-> suc y = n)
58 55, 57 imeqd 
a2 = y -> (a2 e. A -> suc a2 = n <-> y e. A -> suc y = n)
59 58 eale 
A. a2 (a2 e. A -> suc a2 = n) -> y e. A -> suc y = n
60 anrr 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) -> y e. A
61 60 anwl 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x e. A -> y e. A
62 59, 52, 61 sylc 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x e. A -> suc y = n
63 54, 62 eqtr4d 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x e. A -> suc x = suc y
64 28, 63 sylib 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x e. A -> x = y
65 anr 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x = y -> x = y
66 65 eleq1d 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x = y -> (x e. A <-> y e. A)
67 60 anwl 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x = y -> y e. A
68 66, 67 mpbird 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) /\ x = y -> x e. A
69 64, 68 ibida 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) -> (x e. A <-> x = y)
70 69 eqab2d 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) /\ (n = suc y /\ y e. A) -> A == {x | x = y}
71 70 exp 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> n = suc y /\ y e. A -> A == {x | x = y}
72 71 eximd 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> E. y (n = suc y /\ y e. A) -> E. y A == {x | x = y}
73 27, 72 mpd 
A. a3 (E. a2 (a3 = suc a2 /\ a2 e. A) <-> a3 = n) -> E. y A == {x | x = y}
74 11, 73 sylbir 
{a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n} -> E. y A == {x | x = y}
75 74 eex 
E. n {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n} -> E. y A == {x | x = y}
76 3, 75 ax_mp 
~E. y A == {x | x = y} -> ~E. n {a3 | E. a2 (a3 = suc a2 /\ a2 e. A)} == {a1 | a1 = n}
77 2, 76 syl 
~E. y A == {x | x = y} -> theo A = 0

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 (the0), axs_peano (peano2)