numinfctb

Description: A numerable infinite set contains a countable subset.MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015)

		Ref	Expression
	Assertion	numinfctb	$⊢ (S \in dom card \land \neg S \in Fin) \to ω ≼ S$

Step	Hyp	Ref	Expression
1		omelon	$⊢ ω \in On$
2		onenon	$⊢ ω \in On \to ω \in dom card$
3	1 2	ax-mp	$⊢ ω \in dom card$
4		domtri2	$⊢ (ω \in dom card \land S \in dom card) \to (ω ≼ S \leftrightarrow \neg S ≺ ω)$
5	3 4	mpan	$⊢ S \in dom card \to (ω ≼ S \leftrightarrow \neg S ≺ ω)$
6		isfinite	$⊢ S \in Fin \leftrightarrow S ≺ ω$
7	6	notbii	$⊢ \neg S \in Fin \leftrightarrow \neg S ≺ ω$
8	5 7	bitr4di	$⊢ S \in dom card \to (ω ≼ S \leftrightarrow \neg S \in Fin)$
9	8	biimpar	$⊢ (S \in dom card \land \neg S \in Fin) \to ω ≼ S$

Metamath Proof Explorer