Theorem zfcndinf 10687

Description: Axiom of Infinity ax-inf 9707, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5457 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.)

Assertion

Ref	Expression
zfcndinf	⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))

Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Proof of Theorem zfcndinf

Step	Hyp	Ref	Expression
1		el 5457	. . 3 ⊢ ∃𝑤 𝑥 ∈ 𝑤
2		nfv 1913	. . . . . 6 ⊢ Ⅎ𝑤 𝑥 ∈ 𝑦
3		nfe1 2151	. . . . . . . 8 ⊢ Ⅎ𝑤∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)
4	2, 3	nfim 1895	. . . . . . 7 ⊢ Ⅎ𝑤(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))
5	4	nfal 2327	. . . . . 6 ⊢ Ⅎ𝑤∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))
6	2, 5	nfan 1898	. . . . 5 ⊢ Ⅎ𝑤(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
7	6	nfex 2328	. . . 4 ⊢ Ⅎ𝑤∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
8		axinfnd 10675	. . . . 5 ⊢ ∃𝑦(𝑥 ∈ 𝑤 → (𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
9	8	19.37iv 1948	. . . 4 ⊢ (𝑥 ∈ 𝑤 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
10	7, 9	exlimi 2218	. . 3 ⊢ (∃𝑤 𝑥 ∈ 𝑤 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
11	1, 10	ax-mp 5	. 2 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
12		elequ1 2115	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
13		elequ1 2115	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤))
14	13	anbi1d 630	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦) ↔ (𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
15	14	exbidv 1920	. . . . . 6 ⊢ (𝑧 = 𝑥 → (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦) ↔ ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
16	12, 15	imbi12d 344	. . . . 5 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)) ↔ (𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
17	16	cbvalvw 2035	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)) ↔ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
18	17	anbi2i 622	. . 3 ⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
19	18	exbii 1846	. 2 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
20	11, 19	mpbir 231	1 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-13 2380  ax-ext 2711  ax-sep 5317  ax-pr 5447  ax-reg 9661  ax-inf 9707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by: (None)