infordmin

Description: _om is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023)

		Ref	Expression
	Assertion	infordmin	$⊢ \forall x \in (On ∖ Fin) ω \subseteq x$

Step	Hyp	Ref	Expression
1		eldif	$⊢ x \in (On ∖ Fin) \leftrightarrow (x \in On \land \neg x \in Fin)$
2		omelon	$⊢ ω \in On$
3		ontri1	$⊢ (ω \in On \land x \in On) \to (ω \subseteq x \leftrightarrow \neg x \in ω)$
4	3	bicomd	$⊢ (ω \in On \land x \in On) \to (\neg x \in ω \leftrightarrow ω \subseteq x)$
5	4	con1bid	$⊢ (ω \in On \land x \in On) \to (\neg ω \subseteq x \leftrightarrow x \in ω)$
6		nnfi	$⊢ x \in ω \to x \in Fin$
7	5 6	biimtrdi	$⊢ (ω \in On \land x \in On) \to (\neg ω \subseteq x \to x \in Fin)$
8	2 7	mpan	$⊢ x \in On \to (\neg ω \subseteq x \to x \in Fin)$
9	8	con1d	$⊢ x \in On \to (\neg x \in Fin \to ω \subseteq x)$
10	9	imp	$⊢ (x \in On \land \neg x \in Fin) \to ω \subseteq x$
11	1 10	sylbi	$⊢ x \in (On ∖ Fin) \to ω \subseteq x$
12	11	rgen	$⊢ \forall x \in (On ∖ Fin) ω \subseteq x$

Metamath Proof Explorer