Metamath Proof Explorer

Theorem alephiso2

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 alephiso2 
|- aleph Isom _E , ~< ( On , { x e. ran card | _om C_ x } )

Proof

Step Hyp Ref Expression
1 alephiso 
 |-  aleph Isom _E , _E ( On , { x | ( _om C_ x /\ ( card ` x ) = x ) } )
2 iscard4 
 |-  ( ( card ` x ) = x <-> x e. ran card )
3 2 anbi1ci 
 |-  ( ( _om C_ x /\ ( card ` x ) = x ) <-> ( x e. ran card /\ _om C_ x ) )
4 3 abbii 
 |-  { x | ( _om C_ x /\ ( card ` x ) = x ) } = { x | ( x e. ran card /\ _om C_ x ) }
5 df-rab 
 |-  { x e. ran card | _om C_ x } = { x | ( x e. ran card /\ _om C_ x ) }
6 4 5 eqtr4i 
 |-  { x | ( _om C_ x /\ ( card ` x ) = x ) } = { x e. ran card | _om C_ x }
7 f1oeq3 
 |-  ( { x | ( _om C_ x /\ ( card ` x ) = x ) } = { x e. ran card | _om C_ x } -> ( aleph : On -1-1-onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } <-> aleph : On -1-1-onto-> { x e. ran card | _om C_ x } ) )
8 6 7 ax-mp 
 |-  ( aleph : On -1-1-onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } <-> aleph : On -1-1-onto-> { x e. ran card | _om C_ x } )
9 alephon 
 |-  ( aleph ` z ) e. On
10 epelg 
 |-  ( ( aleph ` z ) e. On -> ( ( aleph ` y ) _E ( aleph ` z ) <-> ( aleph ` y ) e. ( aleph ` z ) ) )
11 9 10 mp1i 
 |-  ( ( y e. On /\ z e. On ) -> ( ( aleph ` y ) _E ( aleph ` z ) <-> ( aleph ` y ) e. ( aleph ` z ) ) )
12 alephord2 
 |-  ( ( y e. On /\ z e. On ) -> ( y e. z <-> ( aleph ` y ) e. ( aleph ` z ) ) )
13 alephord 
 |-  ( ( y e. On /\ z e. On ) -> ( y e. z <-> ( aleph ` y ) ~< ( aleph ` z ) ) )
14 11 12 13 3bitr2d 
 |-  ( ( y e. On /\ z e. On ) -> ( ( aleph ` y ) _E ( aleph ` z ) <-> ( aleph ` y ) ~< ( aleph ` z ) ) )
15 14 bibi2d 
 |-  ( ( y e. On /\ z e. On ) -> ( ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) ) <-> ( y _E z <-> ( aleph ` y ) ~< ( aleph ` z ) ) ) )
16 15 ralbidva 
 |-  ( y e. On -> ( A. z e. On ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) ) <-> A. z e. On ( y _E z <-> ( aleph ` y ) ~< ( aleph ` z ) ) ) )
17 16 ralbiia 
 |-  ( A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) ) <-> A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) ~< ( aleph ` z ) ) )
18 8 17 anbi12i 
 |-  ( ( aleph : On -1-1-onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } /\ A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) ) ) <-> ( aleph : On -1-1-onto-> { x e. ran card | _om C_ x } /\ A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) ~< ( aleph ` z ) ) ) )
19 df-isom 
 |-  ( aleph Isom _E , _E ( On , { x | ( _om C_ x /\ ( card ` x ) = x ) } ) <-> ( aleph : On -1-1-onto-> { x | ( _om C_ x /\ ( card ` x ) = x ) } /\ A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) _E ( aleph ` z ) ) ) )
20 df-isom 
 |-  ( aleph Isom _E , ~< ( On , { x e. ran card | _om C_ x } ) <-> ( aleph : On -1-1-onto-> { x e. ran card | _om C_ x } /\ A. y e. On A. z e. On ( y _E z <-> ( aleph ` y ) ~< ( aleph ` z ) ) ) )
21 18 19 20 3bitr4i 
 |-  ( aleph Isom _E , _E ( On , { x | ( _om C_ x /\ ( card ` x ) = x ) } ) <-> aleph Isom _E , ~< ( On , { x e. ran card | _om C_ x } ) )
22 1 21 mpbi 
 |-  aleph Isom _E , ~< ( On , { x e. ran card | _om C_ x } )