Metamath Proof Explorer

Theorem j00smo

Description: _J0 is strictly monotonic over its second argument when its first argument is zero. (Contributed by BTernaryTau, 19-Sep-2026)

Ref Expression
Hypothesis j00smo.1 
|- F = ( x e. On |-> ( _J0 ` <. (/) , x >. ) )
Assertion j00smo 
|- Smo F

Proof

Step Hyp Ref Expression
1 j00smo.1 
 |-  F = ( x e. On |-> ( _J0 ` <. (/) , x >. ) )
2 df-ov 
 |-  ( (/) _J0 x ) = ( _J0 ` <. (/) , x >. )
3 0elon 
 |-  (/) e. On
4 j0iso 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )
5 isof1o 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On )
6 f1of 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On )
7 4 5 6 mp2b 
 |-  _J0 : ( On X. On ) --> On
8 7 fovcl 
 |-  ( ( (/) e. On /\ x e. On ) -> ( (/) _J0 x ) e. On )
9 3 8 mpan 
 |-  ( x e. On -> ( (/) _J0 x ) e. On )
10 2 9 eqeltrrid 
 |-  ( x e. On -> ( _J0 ` <. (/) , x >. ) e. On )
11 1 10 fmpti 
 |-  F : On --> On
12 ordon 
 |-  Ord On
13 0un 
 |-  ( (/) u. y ) = y
14 0un 
 |-  ( (/) u. z ) = z
15 13 14 eleq12i 
 |-  ( ( (/) u. y ) e. ( (/) u. z ) <-> y e. z )
16 orc 
 |-  ( ( (/) u. y ) e. ( (/) u. z ) -> ( ( (/) u. y ) e. ( (/) u. z ) \/ ( ( (/) u. y ) = ( (/) u. z ) /\ <. (/) , y >. LexOrd <. (/) , z >. ) ) )
17 3 a1i 
 |-  ( ( y e. On /\ z e. On ) -> (/) e. On )
18 simpl 
 |-  ( ( y e. On /\ z e. On ) -> y e. On )
19 simpr 
 |-  ( ( y e. On /\ z e. On ) -> z e. On )
20 17 18 17 19 brr0d 
 |-  ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( ( (/) u. y ) e. ( (/) u. z ) \/ ( ( (/) u. y ) = ( (/) u. z ) /\ <. (/) , y >. LexOrd <. (/) , z >. ) ) ) )
21 16 20 imbitrrid 
 |-  ( ( y e. On /\ z e. On ) -> ( ( (/) u. y ) e. ( (/) u. z ) -> <. (/) , y >. _R0 <. (/) , z >. ) )
22 15 21 biimtrrid 
 |-  ( ( y e. On /\ z e. On ) -> ( y e. z -> <. (/) , y >. _R0 <. (/) , z >. ) )
23 opelxpi 
 |-  ( ( (/) e. On /\ y e. On ) -> <. (/) , y >. e. ( On X. On ) )
24 3 23 mpan 
 |-  ( y e. On -> <. (/) , y >. e. ( On X. On ) )
25 opelxpi 
 |-  ( ( (/) e. On /\ z e. On ) -> <. (/) , z >. e. ( On X. On ) )
26 3 25 mpan 
 |-  ( z e. On -> <. (/) , z >. e. ( On X. On ) )
27 isorel 
 |-  ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ ( <. (/) , y >. e. ( On X. On ) /\ <. (/) , z >. e. ( On X. On ) ) ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) )
28 4 27 mpan 
 |-  ( ( <. (/) , y >. e. ( On X. On ) /\ <. (/) , z >. e. ( On X. On ) ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) )
29 24 26 28 syl2an 
 |-  ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) )
30 fvex 
 |-  ( F ` z ) e. _V
31 30 epeli 
 |-  ( ( F ` y ) _E ( F ` z ) <-> ( F ` y ) e. ( F ` z ) )
32 opeq2 
 |-  ( x = y -> <. (/) , x >. = <. (/) , y >. )
33 32 fveq2d 
 |-  ( x = y -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , y >. ) )
34 fvex 
 |-  ( _J0 ` <. (/) , y >. ) e. _V
35 33 1 34 fvmpt 
 |-  ( y e. On -> ( F ` y ) = ( _J0 ` <. (/) , y >. ) )
36 opeq2 
 |-  ( x = z -> <. (/) , x >. = <. (/) , z >. )
37 36 fveq2d 
 |-  ( x = z -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , z >. ) )
38 fvex 
 |-  ( _J0 ` <. (/) , z >. ) e. _V
39 37 1 38 fvmpt 
 |-  ( z e. On -> ( F ` z ) = ( _J0 ` <. (/) , z >. ) )
40 35 39 breqan12d 
 |-  ( ( y e. On /\ z e. On ) -> ( ( F ` y ) _E ( F ` z ) <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) )
41 31 40 bitr3id 
 |-  ( ( y e. On /\ z e. On ) -> ( ( F ` y ) e. ( F ` z ) <-> ( _J0 ` <. (/) , y >. ) _E ( _J0 ` <. (/) , z >. ) ) )
42 29 41 bitr4d 
 |-  ( ( y e. On /\ z e. On ) -> ( <. (/) , y >. _R0 <. (/) , z >. <-> ( F ` y ) e. ( F ` z ) ) )
43 22 42 sylibd 
 |-  ( ( y e. On /\ z e. On ) -> ( y e. z -> ( F ` y ) e. ( F ` z ) ) )
44 11 fdmi 
 |-  dom F = On
45 11 12 43 44 issmo 
 |-  Smo F