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	⊢ ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 )