Theorem zfinf2

Description: A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of BellMachover p. 472. (See ax-inf2 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993)

	Ref	Expression
Assertion	zfinf2	⊢ ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		ax-inf2	⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
2		0el	⊢ ( ∅ ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 )
3		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) )
4	2 3	bitri	⊢ ( ∅ ∈ 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) )
5		sucel	⊢ ( suc 𝑦 ∈ 𝑥 ↔ ∃ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) )
6		df-rex	⊢ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
7	5 6	bitri	⊢ ( suc 𝑦 ∈ 𝑥 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
8	7	ralbii	⊢ ( ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
9		df-ral	⊢ ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
10	8 9	bitri	⊢ ( ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
11	4 10	anbi12i	⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) )
12	11	exbii	⊢ ( ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) )
13	1 12	mpbir	⊢ ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 )