Metamath Proof Explorer

Theorem axinfndlem1

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

Ref Expression
Assertion axinfndlem1 ⊢ ∀ x y ∈ z → ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x

Proof

Step Hyp Ref Expression
1 zfinf ⊢ ∃ w y ∈ w ∧ ∀ y y ∈ w → ∃ z y ∈ z ∧ z ∈ w
2 nfnae ⊢ Ⅎ x ¬ ∀ x x = y
3 nfnae ⊢ Ⅎ x ¬ ∀ x x = z
4 2 3 nfan ⊢ Ⅎ x ¬ ∀ x x = y ∧ ¬ ∀ x x = z
5 nfcvf ⊢ ¬ ∀ x x = y → Ⅎ _ x y
6 5 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x y
7 nfcvd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x w
8 6 7 nfeld ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ w
9 nfnae ⊢ Ⅎ y ¬ ∀ x x = y
10 nfnae ⊢ Ⅎ y ¬ ∀ x x = z
11 9 10 nfan ⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z
12 nfnae ⊢ Ⅎ z ¬ ∀ x x = y
13 nfnae ⊢ Ⅎ z ¬ ∀ x x = z
14 12 13 nfan ⊢ Ⅎ z ¬ ∀ x x = y ∧ ¬ ∀ x x = z
15 nfcvf ⊢ ¬ ∀ x x = z → Ⅎ _ x z
16 15 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ x z
17 6 16 nfeld ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ z
18 16 7 nfeld ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x z ∈ w
19 17 18 nfand ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ z ∧ z ∈ w
20 14 19 nfexd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ z y ∈ z ∧ z ∈ w
21 8 20 nfimd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ w → ∃ z y ∈ z ∧ z ∈ w
22 11 21 nfald ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ y y ∈ w → ∃ z y ∈ z ∧ z ∈ w
23 8 22 nfand ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ w ∧ ∀ y y ∈ w → ∃ z y ∈ z ∧ z ∈ w
24 simpr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → w = x
25 24 eleq2d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → y ∈ w ↔ y ∈ x
26 nfcvd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ y w
27 nfcvf2 ⊢ ¬ ∀ x x = y → Ⅎ _ y x
28 27 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ y x
29 26 28 nfeqd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ y w = x
30 11 29 nfan1 ⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x
31 nfcvd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ z w
32 nfcvf2 ⊢ ¬ ∀ x x = z → Ⅎ _ z x
33 32 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ _ z x
34 31 33 nfeqd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ z w = x
35 14 34 nfan1 ⊢ Ⅎ z ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x
36 elequ2 ⊢ w = x → z ∈ w ↔ z ∈ x
37 36 anbi2d ⊢ w = x → y ∈ z ∧ z ∈ w ↔ y ∈ z ∧ z ∈ x
38 37 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → y ∈ z ∧ z ∈ w ↔ y ∈ z ∧ z ∈ x
39 35 38 exbid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ z y ∈ z ∧ z ∈ w ↔ ∃ z y ∈ z ∧ z ∈ x
40 25 39 imbi12d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → y ∈ w → ∃ z y ∈ z ∧ z ∈ w ↔ y ∈ x → ∃ z y ∈ z ∧ z ∈ x
41 30 40 albid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ y y ∈ w → ∃ z y ∈ z ∧ z ∈ w ↔ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
42 25 41 anbi12d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → y ∈ w ∧ ∀ y y ∈ w → ∃ z y ∈ z ∧ z ∈ w ↔ y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
43 42 ex ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → w = x → y ∈ w ∧ ∀ y y ∈ w → ∃ z y ∈ z ∧ z ∈ w ↔ y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
44 4 23 43 cbvexd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ w y ∈ w ∧ ∀ y y ∈ w → ∃ z y ∈ z ∧ z ∈ w ↔ ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
45 1 44 mpbii ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
46 45 a1d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∀ x y ∈ z → ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
47 46 ex ⊢ ¬ ∀ x x = y → ¬ ∀ x x = z → ∀ x y ∈ z → ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
48 nd1 ⊢ ∀ x x = y → ¬ ∀ x y ∈ z
49 48 pm2.21d ⊢ ∀ x x = y → ∀ x y ∈ z → ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
50 nd2 ⊢ ∀ x x = z → ¬ ∀ x y ∈ z
51 50 pm2.21d ⊢ ∀ x x = z → ∀ x y ∈ z → ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
52 47 49 51 pm2.61ii ⊢ ∀ x y ∈ z → ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x