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 ( ∀ 𝑥 𝑦 ∈ 𝑧 → ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) )

Proof

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