Theorem zfcndinf 10571

Description: Axiom of Infinity ax-inf 9591, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5397 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 5397	. . 3 ⊢ ∃𝑤 𝑥 ∈ 𝑤
2		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑤 𝑥 ∈ 𝑦
3		nfe1 2151	. . . . . . . 8 ⊢ Ⅎ𝑤∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)
4	2, 3	nfim 1896	. . . . . . 7 ⊢ Ⅎ𝑤(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))
5	4	nfal 2322	. . . . . 6 ⊢ Ⅎ𝑤∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))
6	2, 5	nfan 1899	. . . . 5 ⊢ Ⅎ𝑤(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
7	6	nfex 2323	. . . 4 ⊢ Ⅎ𝑤∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
8		axinfnd 10559	. . . . 5 ⊢ ∃𝑦(𝑥 ∈ 𝑤 → (𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
9	8	19.37iv 1948	. . . 4 ⊢ (𝑥 ∈ 𝑤 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
10	7, 9	exlimi 2218	. . 3 ⊢ (∃𝑤 𝑥 ∈ 𝑤 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
11	1, 10	ax-mp 5	. 2 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
12		elequ1 2116	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
13		elequ1 2116	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤))
14	13	anbi1d 631	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦) ↔ (𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
15	14	exbidv 1921	. . . . . 6 ⊢ (𝑧 = 𝑥 → (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦) ↔ ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
16	12, 15	imbi12d 344	. . . . 5 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)) ↔ (𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
17	16	cbvalvw 2036	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)) ↔ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
18	17	anbi2i 623	. . 3 ⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
19	18	exbii 1848	. 2 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥(𝑥 ∈ 𝑦 → ∃𝑤(𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
20	11, 19	mpbir 231	1 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2370  ax-ext 2701  ax-sep 5251  ax-pr 5387  ax-reg 9545  ax-inf 9591

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by: (None)