Metamath Proof Explorer

Theorem omiscard

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

Ref Expression
Assertion omiscard 
|- _om e. ran card

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 nnsdom 
 |-  ( x e. _om -> x ~< _om )
3 sdomnen 
 |-  ( x ~< _om -> -. x ~~ _om )
4 2 3 syl 
 |-  ( x e. _om -> -. x ~~ _om )
5 4 rgen 
 |-  A. x e. _om -. x ~~ _om
6 elrncard 
 |-  ( _om e. ran card <-> ( _om e. On /\ A. x e. _om -. x ~~ _om ) )
7 1 5 6 mpbir2an 
 |-  _om e. ran card