This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inf1

Description: Variation of Axiom of Infinity (using zfinf as a hypothesis). Axiom of Infinity in FreydScedrov p. 283. (Contributed by NM, 14-Oct-1996) (Revised by David Abernethy, 1-Oct-2013)

Ref Expression
Hypothesis inf1.1 ⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
Assertion inf1 ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 inf1.1 ⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
2 ne0i ⊢ ( 𝑦 ∈ 𝑥 → 𝑥 ≠ ∅ )
3 2 anim1i ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) → ( 𝑥 ≠ ∅ ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) )
4 1 3 eximii ⊢ ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )