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