Metamath Proof Explorer

Theorem alephiso3

Description: aleph is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023)

Ref Expression
Assertion alephiso3 
|- aleph Isom _E , ~< ( On , ( ran card \ _om ) )

Proof

Step Hyp Ref Expression
1 alephiso2 
 |-  aleph Isom _E , ~< ( On , { x e. ran card | _om C_ x } )
2 omelon 
 |-  _om e. On
3 elrncard 
 |-  ( x e. ran card <-> ( x e. On /\ A. y e. x -. y ~~ x ) )
4 3 simplbi 
 |-  ( x e. ran card -> x e. On )
5 ontri1 
 |-  ( ( _om e. On /\ x e. On ) -> ( _om C_ x <-> -. x e. _om ) )
6 2 4 5 sylancr 
 |-  ( x e. ran card -> ( _om C_ x <-> -. x e. _om ) )
7 6 rabbiia 
 |-  { x e. ran card | _om C_ x } = { x e. ran card | -. x e. _om }
8 dfdif2 
 |-  ( ran card \ _om ) = { x e. ran card | -. x e. _om }
9 7 8 eqtr4i 
 |-  { x e. ran card | _om C_ x } = ( ran card \ _om )
10 isoeq5 
 |-  ( { x e. ran card | _om C_ x } = ( ran card \ _om ) -> ( aleph Isom _E , ~< ( On , { x e. ran card | _om C_ x } ) <-> aleph Isom _E , ~< ( On , ( ran card \ _om ) ) ) )
11 9 10 ax-mp 
 |-  ( aleph Isom _E , ~< ( On , { x e. ran card | _om C_ x } ) <-> aleph Isom _E , ~< ( On , ( ran card \ _om ) ) )
12 1 11 mpbi 
 |-  aleph Isom _E , ~< ( On , ( ran card \ _om ) )