Theorem omiscard

Description: _om is a cardinal number. (Contributed by RP, 1-Oct-2023)

	Ref	Expression
Assertion	omiscard	⊢ ω ∈ ran card

Proof

Step	Hyp	Ref	Expression
1		omelon	⊢ ω ∈ On
2		nnsdom	⊢ ( 𝑥 ∈ ω → 𝑥 ≺ ω )
3		sdomnen	⊢ ( 𝑥 ≺ ω → ¬ 𝑥 ≈ ω )
4	2 3	syl	⊢ ( 𝑥 ∈ ω → ¬ 𝑥 ≈ ω )
5	4	rgen	⊢ ∀ 𝑥 ∈ ω ¬ 𝑥 ≈ ω
6		elrncard	⊢ ( ω ∈ ran card ↔ ( ω ∈ On ∧ ∀ 𝑥 ∈ ω ¬ 𝑥 ≈ ω ) )
7	1 5 6	mpbir2an	⊢ ω ∈ ran card