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

Metamath Proof Explorer

Theorem infcntss

Description: Every infinite set has a denumerable subset. Similar to Exercise 8 of TakeutiZaring p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.) (Contributed by NM, 23-Oct-2004)

		Ref	Expression
	Hypothesis	infcntss.1	⊢ 𝐴 ∈ V
	Assertion	infcntss	⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω ) )

Proof

Step	Hyp	Ref	Expression
1		infcntss.1	⊢ 𝐴 ∈ V
2	1	domen	⊢ ( ω ≼ 𝐴 ↔ ∃ 𝑥 ( ω ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) )
3		ensym	⊢ ( ω ≈ 𝑥 → 𝑥 ≈ ω )
4	3	anim1ci	⊢ ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω ) )
5	4	eximi	⊢ ( ∃ 𝑥 ( ω ≈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω ) )
6	2 5	sylbi	⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω ) )