Metamath Proof Explorer

Theorem jltalephlem

Description: Lemma for jltaleph . (Contributed by BTernaryTau, 16-Oct-2026)

Ref Expression
Assertion jltalephlem 
|- ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) )

Proof

Step Hyp Ref Expression
1 9on 
 |-  9o e. On
2 j0iso 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )
3 isof1o 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On )
4 f1of 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On )
5 2 3 4 mp2b 
 |-  _J0 : ( On X. On ) --> On
6 0elon 
 |-  (/) e. On
7 5 6 f0cli 
 |-  ( _J0 ` <. A , B >. ) e. On
8 omxpen 
 |-  ( ( 9o e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( 9o X. ( _J0 ` <. A , B >. ) ) )
9 1 7 8 mp2an 
 |-  ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( 9o X. ( _J0 ` <. A , B >. ) )
10 9onn 
 |-  9o e. _om
11 10 elexi 
 |-  9o e. _V
12 fvex 
 |-  ( _J0 ` <. A , B >. ) e. _V
13 11 12 xpcomen 
 |-  ( 9o X. ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o )
14 9 13 entri 
 |-  ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o )
15 nnfi 
 |-  ( 9o e. _om -> 9o e. Fin )
16 fict 
 |-  ( 9o e. Fin -> 9o ~<_ _om )
17 10 15 16 mp2b 
 |-  9o ~<_ _om
18 domtr 
 |-  ( ( 9o ~<_ _om /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> 9o ~<_ ( _J0 ` <. A , B >. ) )
19 17 18 mpan 
 |-  ( _om ~<_ ( _J0 ` <. A , B >. ) -> 9o ~<_ ( _J0 ` <. A , B >. ) )
20 df-9o 
 |-  9o = suc 8o
21 nsuceq0 
 |-  suc 8o =/= (/)
22 20 21 eqnetri 
 |-  9o =/= (/)
23 onenon 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( _J0 ` <. A , B >. ) e. dom card )
24 7 23 ax-mp 
 |-  ( _J0 ` <. A , B >. ) e. dom card
25 infxpabs 
 |-  ( ( ( ( _J0 ` <. A , B >. ) e. dom card /\ _om ~<_ ( _J0 ` <. A , B >. ) ) /\ ( 9o =/= (/) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) )
26 24 25 mpanl1 
 |-  ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( 9o =/= (/) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) )
27 22 26 mpanr1 
 |-  ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) )
28 19 27 mpdan 
 |-  ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) )
29 entr 
 |-  ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o ) /\ ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) )
30 14 28 29 sylancr 
 |-  ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) )
31 ensym 
 |-  ( ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) )
32 domentr 
 |-  ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( _J0 ` <. A , B >. ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) )
33 31 32 sylan2 
 |-  ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) )
34 30 33 mpdan 
 |-  ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) )
35 omcl 
 |-  ( ( 9o e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. On )
36 1 7 35 mp2an 
 |-  ( 9o .o ( _J0 ` <. A , B >. ) ) e. On
37 1 oneli 
 |-  ( C e. 9o -> C e. On )
38 onadju 
 |-  ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. On /\ C e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) )
39 36 37 38 sylancr 
 |-  ( C e. 9o -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) )
40 onenon 
 |-  ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. On -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card )
41 36 40 ax-mp 
 |-  ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card
42 simpr 
 |-  ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) )
43 elnn 
 |-  ( ( C e. 9o /\ 9o e. _om ) -> C e. _om )
44 10 43 mpan2 
 |-  ( C e. 9o -> C e. _om )
45 nnfi 
 |-  ( C e. _om -> C e. Fin )
46 fict 
 |-  ( C e. Fin -> C ~<_ _om )
47 44 45 46 3syl 
 |-  ( C e. 9o -> C ~<_ _om )
48 domtr 
 |-  ( ( C ~<_ _om /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) )
49 47 48 sylan 
 |-  ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) )
50 infdjuabs 
 |-  ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) /\ C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) )
51 41 42 49 50 mp3an2i 
 |-  ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) )
52 entr 
 |-  ( ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) /\ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) )
53 39 51 52 syl2an2r 
 |-  ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) )
54 34 53 sylan2 
 |-  ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) )
55 30 adantl 
 |-  ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) )
56 entr 
 |-  ( ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) /\ ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) )
57 54 55 56 syl2anc 
 |-  ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) )