# 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$