Theorem omssrncard

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

	Ref	Expression
Assertion	omssrncard	|- _om C_ ran card

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( x e. _om -> x e. On )
2		onelon	|- ( ( x e. On /\ y e. x ) -> y e. On )
3		simpl	|- ( ( x e. On /\ y e. x ) -> x e. On )
4		simpr	|- ( ( x e. On /\ y e. x ) -> y e. x )
5		onelpss	|- ( ( y e. On /\ x e. On ) -> ( y e. x <-> ( y C_ x /\ y =/= x ) ) )
6	5	biimpa	|- ( ( ( y e. On /\ x e. On ) /\ y e. x ) -> ( y C_ x /\ y =/= x ) )
7	2 3 4 6	syl21anc	|- ( ( x e. On /\ y e. x ) -> ( y C_ x /\ y =/= x ) )
8		df-pss	|- ( y C. x <-> ( y C_ x /\ y =/= x ) )
9	7 8	sylibr	|- ( ( x e. On /\ y e. x ) -> y C. x )
10	9	ex	|- ( x e. On -> ( y e. x -> y C. x ) )
11	1 10	syl	|- ( x e. _om -> ( y e. x -> y C. x ) )
12	11	imdistani	|- ( ( x e. _om /\ y e. x ) -> ( x e. _om /\ y C. x ) )
13		php	|- ( ( x e. _om /\ y C. x ) -> -. x ~~ y )
14	12 13	syl	|- ( ( x e. _om /\ y e. x ) -> -. x ~~ y )
15		ensymb	|- ( x ~~ y <-> y ~~ x )
16	14 15	sylnib	|- ( ( x e. _om /\ y e. x ) -> -. y ~~ x )
17	16	ralrimiva	|- ( x e. _om -> A. y e. x -. y ~~ x )
18		elrncard	|- ( x e. ran card <-> ( x e. On /\ A. y e. x -. y ~~ x ) )
19	1 17 18	sylanbrc	|- ( x e. _om -> x e. ran card )
20	19	ssriv	|- _om C_ ran card