Theorem omssrncard

Description: All natural numbers are cardinals. (Contributed by RP, 1-Oct-2023)

	Ref	Expression
Assertion	omssrncard	⊢ ω ⊆ ran card

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
2		onelon	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
3		simpl	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ On )
4		simpr	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
5		onelpss	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥 ) ) )
6	5	biimpa	⊢ ( ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥 ) )
7	2 3 4 6	syl21anc	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥 ) )
8		df-pss	⊢ ( 𝑦 ⊊ 𝑥 ↔ ( 𝑦 ⊆ 𝑥 ∧ 𝑦 ≠ 𝑥 ) )
9	7 8	sylibr	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ⊊ 𝑥 )
10	9	ex	⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → 𝑦 ⊊ 𝑥 ) )
11	1 10	syl	⊢ ( 𝑥 ∈ ω → ( 𝑦 ∈ 𝑥 → 𝑦 ⊊ 𝑥 ) )
12	11	imdistani	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ∈ ω ∧ 𝑦 ⊊ 𝑥 ) )
13		php	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ⊊ 𝑥 ) → ¬ 𝑥 ≈ 𝑦 )
14	12 13	syl	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑥 ≈ 𝑦 )
15		ensymb	⊢ ( 𝑥 ≈ 𝑦 ↔ 𝑦 ≈ 𝑥 )
16	14 15	sylnib	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑦 ≈ 𝑥 )
17	16	ralrimiva	⊢ ( 𝑥 ∈ ω → ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ≈ 𝑥 )
18		elrncard	⊢ ( 𝑥 ∈ ran card ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ≈ 𝑥 ) )
19	1 17 18	sylanbrc	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ ran card )
20	19	ssriv	⊢ ω ⊆ ran card