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

Metamath Proof Explorer

Theorem inf2

Description: Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf as a hypothesis). Abbreviated version of the Axiom of Infinity in FreydScedrov p. 283. (Contributed by NM, 28-Oct-1996)

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

Proof

Step Hyp Ref Expression
1 inf1.1 ⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
2 1 inf1 ⊢ ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
3 df-ss ⊢ ( 𝑥 ⊆ ∪ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∪ 𝑥 ) )
4 eluni ⊢ ( 𝑦 ∈ ∪ 𝑥 ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) )
5 4 imbi2i ⊢ ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∪ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
6 5 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∪ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
7 3 6 bitri ⊢ ( 𝑥 ⊆ ∪ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
8 7 anbi2i ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ( 𝑥 ≠ ∅ ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) )
9 8 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) )
10 2 9 mpbir ⊢ ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 )