Metamath Proof Explorer

Theorem j0ltalephlem

Description: Lemma for j0ltaleph . (Contributed by BTernaryTau, 25-Sep-2026)

Ref Expression
Assertion j0ltalephlem 
|- ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( _J0 ` <. A , B >. ) e. _V
2 j0iso 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )
3 opelxpi 
 |-  ( ( A e. On /\ B e. On ) -> <. A , B >. e. ( On X. On ) )
4 imassrn 
 |-  ( `' _R0 " { <. A , B >. } ) C_ ran `' _R0
5 dfdm4 
 |-  dom _R0 = ran `' _R0
6 dmr0ss 
 |-  dom _R0 C_ ( On X. On )
7 5 6 eqsstrri 
 |-  ran `' _R0 C_ ( On X. On )
8 4 7 sstri 
 |-  ( `' _R0 " { <. A , B >. } ) C_ ( On X. On )
9 sseqin2 
 |-  ( ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) <-> ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) = ( `' _R0 " { <. A , B >. } ) )
10 8 9 mpbi 
 |-  ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) = ( `' _R0 " { <. A , B >. } )
11 10 eqcomi 
 |-  ( `' _R0 " { <. A , B >. } ) = ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) )
12 1 epini 
 |-  ( `' _E " { ( _J0 ` <. A , B >. ) } ) = ( _J0 ` <. A , B >. )
13 12 ineq2i 
 |-  ( On i^i ( `' _E " { ( _J0 ` <. A , B >. ) } ) ) = ( On i^i ( _J0 ` <. A , B >. ) )
14 isof1o 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On )
15 f1of 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On )
16 2 14 15 mp2b 
 |-  _J0 : ( On X. On ) --> On
17 0elon 
 |-  (/) e. On
18 16 17 f0cli 
 |-  ( _J0 ` <. A , B >. ) e. On
19 18 onssi 
 |-  ( _J0 ` <. A , B >. ) C_ On
20 sseqin2 
 |-  ( ( _J0 ` <. A , B >. ) C_ On <-> ( On i^i ( _J0 ` <. A , B >. ) ) = ( _J0 ` <. A , B >. ) )
21 19 20 mpbi 
 |-  ( On i^i ( _J0 ` <. A , B >. ) ) = ( _J0 ` <. A , B >. )
22 13 21 eqtr2i 
 |-  ( _J0 ` <. A , B >. ) = ( On i^i ( `' _E " { ( _J0 ` <. A , B >. ) } ) )
23 11 22 isoini2 
 |-  ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ <. A , B >. e. ( On X. On ) ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) )
24 2 3 23 sylancr 
 |-  ( ( A e. On /\ B e. On ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) )
25 isof1o 
 |-  ( ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( `' _R0 " { <. A , B >. } ) -1-1-onto-> ( _J0 ` <. A , B >. ) )
26 f1ocnv 
 |-  ( ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( `' _R0 " { <. A , B >. } ) -1-1-onto-> ( _J0 ` <. A , B >. ) -> `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) )
27 24 25 26 3syl 
 |-  ( ( A e. On /\ B e. On ) -> `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) )
28 f1oeng 
 |-  ( ( ( _J0 ` <. A , B >. ) e. _V /\ `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) ) -> ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) )
29 1 27 28 sylancr 
 |-  ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) )
30 onun2 
 |-  ( ( A e. On /\ B e. On ) -> ( A u. B ) e. On )
31 onsuc 
 |-  ( ( A u. B ) e. On -> suc ( A u. B ) e. On )
32 30 31 syl 
 |-  ( ( A e. On /\ B e. On ) -> suc ( A u. B ) e. On )
33 32 32 xpexd 
 |-  ( ( A e. On /\ B e. On ) -> ( suc ( A u. B ) X. suc ( A u. B ) ) e. _V )
34 simplrl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x e. On )
35 simplrr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y e. On )
36 simplll 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> A e. On )
37 simpllr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> B e. On )
38 opex 
 |-  <. A , B >. e. _V
39 opex 
 |-  <. x , y >. e. _V
40 39 eliniseg 
 |-  ( <. A , B >. e. _V -> ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) <-> <. x , y >. _R0 <. A , B >. ) )
41 38 40 ax-mp 
 |-  ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) <-> <. x , y >. _R0 <. A , B >. )
42 41 bilani 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> <. x , y >. _R0 <. A , B >. )
43 34 35 36 37 42 r0maxss 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( x u. y ) C_ ( A u. B ) )
44 43 unssad 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x C_ ( A u. B ) )
45 36 37 30 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( A u. B ) e. On )
46 onsssuc 
 |-  ( ( x e. On /\ ( A u. B ) e. On ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) )
47 34 45 46 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) )
48 44 47 mpbid 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x e. suc ( A u. B ) )
49 43 unssbd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y C_ ( A u. B ) )
50 onsssuc 
 |-  ( ( y e. On /\ ( A u. B ) e. On ) -> ( y C_ ( A u. B ) <-> y e. suc ( A u. B ) ) )
51 35 45 50 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( y C_ ( A u. B ) <-> y e. suc ( A u. B ) ) )
52 49 51 mpbid 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y e. suc ( A u. B ) )
53 48 52 opelxpd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) )
54 53 ex 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) -> ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) )
55 54 ralrimivva 
 |-  ( ( A e. On /\ B e. On ) -> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) )
56 ssrel2 
 |-  ( ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) -> ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) <-> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) )
57 8 56 ax-mp 
 |-  ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) <-> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) )
58 55 57 sylibr 
 |-  ( ( A e. On /\ B e. On ) -> ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) )
59 ssdomg 
 |-  ( ( suc ( A u. B ) X. suc ( A u. B ) ) e. _V -> ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) -> ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) )
60 33 58 59 sylc 
 |-  ( ( A e. On /\ B e. On ) -> ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) )
61 endomtr 
 |-  ( ( ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) /\ ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) )
62 29 60 61 syl2anc 
 |-  ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) )