Theorem infordmin

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

	Ref	Expression
Assertion	infordmin	⊢ ∀ 𝑥 ∈ ( On ∖ Fin ) ω ⊆ 𝑥

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝑥 ∈ ( On ∖ Fin ) ↔ ( 𝑥 ∈ On ∧ ¬ 𝑥 ∈ Fin ) )
2		omelon	⊢ ω ∈ On
3		ontri1	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ω ) )
4	3	bicomd	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑥 ∈ ω ↔ ω ⊆ 𝑥 ) )
5	4	con1bid	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ¬ ω ⊆ 𝑥 ↔ 𝑥 ∈ ω ) )
6		nnfi	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
7	5 6	syl6bi	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ¬ ω ⊆ 𝑥 → 𝑥 ∈ Fin ) )
8	2 7	mpan	⊢ ( 𝑥 ∈ On → ( ¬ ω ⊆ 𝑥 → 𝑥 ∈ Fin ) )
9	8	con1d	⊢ ( 𝑥 ∈ On → ( ¬ 𝑥 ∈ Fin → ω ⊆ 𝑥 ) )
10	9	imp	⊢ ( ( 𝑥 ∈ On ∧ ¬ 𝑥 ∈ Fin ) → ω ⊆ 𝑥 )
11	1 10	sylbi	⊢ ( 𝑥 ∈ ( On ∖ Fin ) → ω ⊆ 𝑥 )
12	11	rgen	⊢ ∀ 𝑥 ∈ ( On ∖ Fin ) ω ⊆ 𝑥