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

Proof

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