Metamath Proof Explorer

Theorem j0iso

Description: _J0 is the _R0 order isomorphism of On X. On onto On . Definition 7.59 of TakeutiZaring p. 55. This isomorphism is unique by weisoeq and r0weseon . (Contributed by BTernaryTau, 19-Sep-2026)

Ref Expression
Assertion j0iso 
|- _J0 Isom _R0 , _E ( ( On X. On ) , On )

Proof

Step Hyp Ref Expression
1 r0weseon 
 |-  ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) )
2 onprc 
 |-  -. On e. _V
3 xpexr 
 |-  ( ( On X. On ) e. _V -> ( On e. _V \/ On e. _V ) )
4 pm1.2 
 |-  ( ( On e. _V \/ On e. _V ) -> On e. _V )
5 3 4 syl 
 |-  ( ( On X. On ) e. _V -> On e. _V )
6 2 5 mto 
 |-  -. ( On X. On ) e. _V
7 eqid 
 |-  OrdIso ( _R0 , ( On X. On ) ) = OrdIso ( _R0 , ( On X. On ) )
8 7 ordtypeon 
 |-  ( ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) /\ -. ( On X. On ) e. _V ) -> OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) )
9 6 8 mp3an3 
 |-  ( ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) -> OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) )
10 isocnv 
 |-  ( OrdIso ( _R0 , ( On X. On ) ) Isom _E , _R0 ( On , ( On X. On ) ) -> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) )
11 1 9 10 mp2b 
 |-  `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On )
12 df-j0 
 |-  _J0 = `' OrdIso ( _R0 , ( On X. On ) )
13 isoeq1 
 |-  ( _J0 = `' OrdIso ( _R0 , ( On X. On ) ) -> ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) <-> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) ) )
14 12 13 ax-mp 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) <-> `' OrdIso ( _R0 , ( On X. On ) ) Isom _R0 , _E ( ( On X. On ) , On ) )
15 11 14 mpbir 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )