Metamath Proof Explorer


Theorem axinfnd

Description: A version of the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002)

Ref Expression
Assertion axinfnd x y z y x y y x z y z z x

Proof

Step Hyp Ref Expression
1 axinfndlem1 x w z x w x w w x z w z z x
2 1 ax-gen w x w z x w x w w x z w z z x
3 nfnae y ¬ y y = x
4 nfnae y ¬ y y = z
5 3 4 nfan y ¬ y y = x ¬ y y = z
6 nfnae x ¬ y y = x
7 nfnae x ¬ y y = z
8 6 7 nfan x ¬ y y = x ¬ y y = z
9 nfcvd ¬ y y = x ¬ y y = z _ y w
10 nfcvf ¬ y y = z _ y z
11 10 adantl ¬ y y = x ¬ y y = z _ y z
12 9 11 nfeld ¬ y y = x ¬ y y = z y w z
13 8 12 nfald ¬ y y = x ¬ y y = z y x w z
14 nfcvf ¬ y y = x _ y x
15 14 adantr ¬ y y = x ¬ y y = z _ y x
16 9 15 nfeld ¬ y y = x ¬ y y = z y w x
17 nfnae w ¬ y y = x
18 nfnae w ¬ y y = z
19 17 18 nfan w ¬ y y = x ¬ y y = z
20 nfnae z ¬ y y = x
21 nfnae z ¬ y y = z
22 20 21 nfan z ¬ y y = x ¬ y y = z
23 11 15 nfeld ¬ y y = x ¬ y y = z y z x
24 12 23 nfand ¬ y y = x ¬ y y = z y w z z x
25 22 24 nfexd ¬ y y = x ¬ y y = z y z w z z x
26 16 25 nfimd ¬ y y = x ¬ y y = z y w x z w z z x
27 19 26 nfald ¬ y y = x ¬ y y = z y w w x z w z z x
28 16 27 nfand ¬ y y = x ¬ y y = z y w x w w x z w z z x
29 8 28 nfexd ¬ y y = x ¬ y y = z y x w x w w x z w z z x
30 13 29 nfimd ¬ y y = x ¬ y y = z y x w z x w x w w x z w z z x
31 nfcvd ¬ y y = x ¬ y y = z _ x w
32 nfcvf2 ¬ y y = x _ x y
33 32 adantr ¬ y y = x ¬ y y = z _ x y
34 31 33 nfeqd ¬ y y = x ¬ y y = z x w = y
35 8 34 nfan1 x ¬ y y = x ¬ y y = z w = y
36 simpr ¬ y y = x ¬ y y = z w = y w = y
37 36 eleq1d ¬ y y = x ¬ y y = z w = y w z y z
38 35 37 albid ¬ y y = x ¬ y y = z w = y x w z x y z
39 36 eleq1d ¬ y y = x ¬ y y = z w = y w x y x
40 nfcvd ¬ y y = x ¬ y y = z _ z w
41 nfcvf2 ¬ y y = z _ z y
42 41 adantl ¬ y y = x ¬ y y = z _ z y
43 40 42 nfeqd ¬ y y = x ¬ y y = z z w = y
44 22 43 nfan1 z ¬ y y = x ¬ y y = z w = y
45 37 anbi1d ¬ y y = x ¬ y y = z w = y w z z x y z z x
46 44 45 exbid ¬ y y = x ¬ y y = z w = y z w z z x z y z z x
47 39 46 imbi12d ¬ y y = x ¬ y y = z w = y w x z w z z x y x z y z z x
48 47 ex ¬ y y = x ¬ y y = z w = y w x z w z z x y x z y z z x
49 5 26 48 cbvald ¬ y y = x ¬ y y = z w w x z w z z x y y x z y z z x
50 49 adantr ¬ y y = x ¬ y y = z w = y w w x z w z z x y y x z y z z x
51 39 50 anbi12d ¬ y y = x ¬ y y = z w = y w x w w x z w z z x y x y y x z y z z x
52 35 51 exbid ¬ y y = x ¬ y y = z w = y x w x w w x z w z z x x y x y y x z y z z x
53 38 52 imbi12d ¬ y y = x ¬ y y = z w = y x w z x w x w w x z w z z x x y z x y x y y x z y z z x
54 53 ex ¬ y y = x ¬ y y = z w = y x w z x w x w w x z w z z x x y z x y x y y x z y z z x
55 5 30 54 cbvald ¬ y y = x ¬ y y = z w x w z x w x w w x z w z z x y x y z x y x y y x z y z z x
56 2 55 mpbii ¬ y y = x ¬ y y = z y x y z x y x y y x z y z z x
57 56 19.21bi ¬ y y = x ¬ y y = z x y z x y x y y x z y z z x
58 57 ex ¬ y y = x ¬ y y = z x y z x y x y y x z y z z x
59 nd1 x x = y ¬ x y z
60 59 aecoms y y = x ¬ x y z
61 60 pm2.21d y y = x x y z x y x y y x z y z z x
62 nd3 y y = z ¬ x y z
63 62 pm2.21d y y = z x y z x y x y y x z y z z x
64 58 61 63 pm2.61ii x y z x y x y y x z y z z x
65 64 19.35ri x y z y x y y x z y z z x