Theorem zfcndinf

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

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

Proof

Step	Hyp	Ref	Expression
1		el	⊢ ∃ 𝑤 𝑥 ∈ 𝑤
2		nfv	⊢ Ⅎ 𝑤 𝑥 ∈ 𝑦
3		nfe1	⊢ Ⅎ 𝑤 ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 )
4	2 3	nfim	⊢ Ⅎ 𝑤 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) )
5	4	nfal	⊢ Ⅎ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) )
6	2 5	nfan	⊢ Ⅎ 𝑤 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )
7	6	nfex	⊢ Ⅎ 𝑤 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )
8		axinfnd	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑤 → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
9	8	19.37iv	⊢ ( 𝑥 ∈ 𝑤 → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
10	7 9	exlimi	⊢ ( ∃ 𝑤 𝑥 ∈ 𝑤 → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
11	1 10	ax-mp	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )
12		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
13		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤 ) )
14	13	anbi1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )
15	14	exbidv	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ↔ ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )
16	12 15	imbi12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
17	16	cbvalvw	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )
18	17	anbi2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
19	18	exbii	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ∃ 𝑤 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) ) )
20	11 19	mpbir	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) ) )