Metamath Proof Explorer

Theorem maxssj0

Description: The value of _J0 is at least the maximum of its two arguments. Proposition 15.1(1) of TakeutiZaring p. 154. (Contributed by BTernaryTau, 22-Sep-2026)

Ref Expression
Assertion maxssj0 
|- ( ( A e. On /\ B e. On ) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) )

Proof

Step Hyp Ref Expression
1 j0iso 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )
2 isof1o 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On )
3 f1of 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On )
4 1 2 3 mp2b 
 |-  _J0 : ( On X. On ) --> On
5 0elon 
 |-  (/) e. On
6 4 5 f0cli 
 |-  ( _J0 ` <. A , B >. ) e. On
7 5 a1i 
 |-  ( ( A e. On /\ B e. On ) -> (/) e. On )
8 onun2 
 |-  ( ( A e. On /\ B e. On ) -> ( A u. B ) e. On )
9 7 8 opelxpd 
 |-  ( ( A e. On /\ B e. On ) -> <. (/) , ( A u. B ) >. e. ( On X. On ) )
10 opelxpi 
 |-  ( ( A e. On /\ B e. On ) -> <. A , B >. e. ( On X. On ) )
11 isorel 
 |-  ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ ( <. (/) , ( A u. B ) >. e. ( On X. On ) /\ <. A , B >. e. ( On X. On ) ) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) )
12 1 11 mpan 
 |-  ( ( <. (/) , ( A u. B ) >. e. ( On X. On ) /\ <. A , B >. e. ( On X. On ) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) )
13 9 10 12 syl2anc 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) ) )
14 fvex 
 |-  ( _J0 ` <. A , B >. ) e. _V
15 14 epeli 
 |-  ( ( _J0 ` <. (/) , ( A u. B ) >. ) _E ( _J0 ` <. A , B >. ) <-> ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) )
16 13 15 bitrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) )
17 fvex 
 |-  ( _J0 ` <. (/) , x >. ) e. _V
18 eqid 
 |-  ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) = ( x e. On |-> ( _J0 ` <. (/) , x >. ) )
19 17 18 fnmpti 
 |-  ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) Fn On
20 18 j00smo 
 |-  Smo ( x e. On |-> ( _J0 ` <. (/) , x >. ) )
21 smogt 
 |-  ( ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) Fn On /\ Smo ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) /\ ( A u. B ) e. On ) -> ( A u. B ) C_ ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) )
22 19 20 21 mp3an12 
 |-  ( ( A u. B ) e. On -> ( A u. B ) C_ ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) )
23 opeq2 
 |-  ( x = ( A u. B ) -> <. (/) , x >. = <. (/) , ( A u. B ) >. )
24 23 fveq2d 
 |-  ( x = ( A u. B ) -> ( _J0 ` <. (/) , x >. ) = ( _J0 ` <. (/) , ( A u. B ) >. ) )
25 fvex 
 |-  ( _J0 ` <. (/) , ( A u. B ) >. ) e. _V
26 24 18 25 fvmpt 
 |-  ( ( A u. B ) e. On -> ( ( x e. On |-> ( _J0 ` <. (/) , x >. ) ) ` ( A u. B ) ) = ( _J0 ` <. (/) , ( A u. B ) >. ) )
27 22 26 sseqtrd 
 |-  ( ( A u. B ) e. On -> ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) )
28 8 27 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) )
29 ontr2 
 |-  ( ( ( A u. B ) e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) /\ ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) )
30 8 6 29 sylancl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) /\ ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) )
31 28 30 mpand 
 |-  ( ( A e. On /\ B e. On ) -> ( ( _J0 ` <. (/) , ( A u. B ) >. ) e. ( _J0 ` <. A , B >. ) -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) )
32 16 31 sylbid 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. -> ( A u. B ) e. ( _J0 ` <. A , B >. ) ) )
33 onelss 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( ( A u. B ) e. ( _J0 ` <. A , B >. ) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) )
34 6 32 33 mpsylsyld 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) )
35 eqcom 
 |-  ( A = (/) <-> (/) = A )
36 35 biimpi 
 |-  ( A = (/) -> (/) = A )
37 uneq1 
 |-  ( A = (/) -> ( A u. B ) = ( (/) u. B ) )
38 0un 
 |-  ( (/) u. B ) = B
39 37 38 eqtrdi 
 |-  ( A = (/) -> ( A u. B ) = B )
40 36 39 opeq12d 
 |-  ( A = (/) -> <. (/) , ( A u. B ) >. = <. A , B >. )
41 40 fveq2d 
 |-  ( A = (/) -> ( _J0 ` <. (/) , ( A u. B ) >. ) = ( _J0 ` <. A , B >. ) )
42 41 sseq2d 
 |-  ( A = (/) -> ( ( A u. B ) C_ ( _J0 ` <. (/) , ( A u. B ) >. ) <-> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) )
43 28 42 syl5ibcom 
 |-  ( ( A e. On /\ B e. On ) -> ( A = (/) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) ) )
44 0un 
 |-  ( (/) u. ( A u. B ) ) = ( A u. B )
45 44 a1i 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) u. ( A u. B ) ) = ( A u. B ) )
46 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
47 simpr 
 |-  ( ( A e. On /\ B e. On ) -> B e. On )
48 7 8 46 47 brr0d 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) ) )
49 eloni 
 |-  ( ( A u. B ) e. On -> Ord ( A u. B ) )
50 ordirr 
 |-  ( Ord ( A u. B ) -> -. ( A u. B ) e. ( A u. B ) )
51 8 49 50 3syl 
 |-  ( ( A e. On /\ B e. On ) -> -. ( A u. B ) e. ( A u. B ) )
52 44 eleq1i 
 |-  ( ( (/) u. ( A u. B ) ) e. ( A u. B ) <-> ( A u. B ) e. ( A u. B ) )
53 51 52 sylnibr 
 |-  ( ( A e. On /\ B e. On ) -> -. ( (/) u. ( A u. B ) ) e. ( A u. B ) )
54 orel1 
 |-  ( -. ( (/) u. ( A u. B ) ) e. ( A u. B ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) -> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) )
55 olc 
 |-  ( ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) -> ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) )
56 54 55 impbid1 
 |-  ( -. ( (/) u. ( A u. B ) ) e. ( A u. B ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) )
57 53 56 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( ( (/) u. ( A u. B ) ) e. ( A u. B ) \/ ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) )
58 48 57 bitrd 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> ( ( (/) u. ( A u. B ) ) = ( A u. B ) /\ <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) ) )
59 45 58 mpbirand 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> <. (/) , ( A u. B ) >. LexOrd <. A , B >. ) )
60 7 8 46 47 brlexod 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. LexOrd <. A , B >. <-> ( (/) e. A \/ ( (/) = A /\ ( A u. B ) e. B ) ) ) )
61 eloni 
 |-  ( B e. On -> Ord B )
62 ordirr 
 |-  ( Ord B -> -. B e. B )
63 61 62 syl 
 |-  ( B e. On -> -. B e. B )
64 63 intnand 
 |-  ( B e. On -> -. ( A e. B /\ B e. B ) )
65 64 adantl 
 |-  ( ( A e. On /\ B e. On ) -> -. ( A e. B /\ B e. B ) )
66 onunel 
 |-  ( ( A e. On /\ B e. On /\ B e. On ) -> ( ( A u. B ) e. B <-> ( A e. B /\ B e. B ) ) )
67 66 3anidm23 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A u. B ) e. B <-> ( A e. B /\ B e. B ) ) )
68 65 67 mtbird 
 |-  ( ( A e. On /\ B e. On ) -> -. ( A u. B ) e. B )
69 68 intnand 
 |-  ( ( A e. On /\ B e. On ) -> -. ( (/) = A /\ ( A u. B ) e. B ) )
70 orel2 
 |-  ( -. ( (/) = A /\ ( A u. B ) e. B ) -> ( ( (/) e. A \/ ( (/) = A /\ ( A u. B ) e. B ) ) -> (/) e. A ) )
71 orc 
 |-  ( (/) e. A -> ( (/) e. A \/ ( (/) = A /\ ( A u. B ) e. B ) ) )
72 70 71 impbid1 
 |-  ( -. ( (/) = A /\ ( A u. B ) e. B ) -> ( ( (/) e. A \/ ( (/) = A /\ ( A u. B ) e. B ) ) <-> (/) e. A ) )
73 69 72 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( (/) e. A \/ ( (/) = A /\ ( A u. B ) e. B ) ) <-> (/) e. A ) )
74 59 60 73 3bitrd 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> (/) e. A ) )
75 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
76 75 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. A <-> A =/= (/) ) )
77 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
78 76 77 bitrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. A <-> -. A = (/) ) )
79 74 78 bitrd 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) )
80 xor3 
 |-  ( -. ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> A = (/) ) <-> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) )
81 nbior 
 |-  ( -. ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> A = (/) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) )
82 80 81 sylbir 
 |-  ( ( <. (/) , ( A u. B ) >. _R0 <. A , B >. <-> -. A = (/) ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) )
83 79 82 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( <. (/) , ( A u. B ) >. _R0 <. A , B >. \/ A = (/) ) )
84 34 43 83 mpjaod 
 |-  ( ( A e. On /\ B e. On ) -> ( A u. B ) C_ ( _J0 ` <. A , B >. ) )