Metamath Proof Explorer

Theorem j0ltaleph

Description: The value of _J0 is less than an aleph if its two arguments are less than that aleph. Proposition 15.1(2) of TakeutiZaring p. 154. (Contributed by BTernaryTau, 25-Sep-2026)

Ref Expression
Assertion j0ltaleph 
|- ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) )

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om 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 domtriord 
 |-  ( ( _om e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) <-> -. ( _J0 ` <. A , B >. ) ~< _om ) )
9 1 7 8 mp2an 
 |-  ( _om ~<_ ( _J0 ` <. A , B >. ) <-> -. ( _J0 ` <. A , B >. ) ~< _om )
10 9 con2bii 
 |-  ( ( _J0 ` <. A , B >. ) ~< _om <-> -. _om ~<_ ( _J0 ` <. A , B >. ) )
11 sdomel 
 |-  ( ( ( _J0 ` <. A , B >. ) e. On /\ _om e. On ) -> ( ( _J0 ` <. A , B >. ) ~< _om -> ( _J0 ` <. A , B >. ) e. _om ) )
12 7 1 11 mp2an 
 |-  ( ( _J0 ` <. A , B >. ) ~< _om -> ( _J0 ` <. A , B >. ) e. _om )
13 10 12 sylbir 
 |-  ( -. _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) e. _om )
14 13 orri 
 |-  ( _om ~<_ ( _J0 ` <. A , B >. ) \/ ( _J0 ` <. A , B >. ) e. _om )
15 alephon 
 |-  ( aleph ` C ) e. On
16 15 oneli 
 |-  ( A e. ( aleph ` C ) -> A e. On )
17 15 oneli 
 |-  ( B e. ( aleph ` C ) -> B e. On )
18 16 17 anim12i 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( A e. On /\ B e. On ) )
19 18 3adant3 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( A e. On /\ B e. On ) )
20 j0ltalephlem 
 |-  ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) )
21 xpfi 
 |-  ( ( suc ( A u. B ) e. Fin /\ suc ( A u. B ) e. Fin ) -> ( suc ( A u. B ) X. suc ( A u. B ) ) e. Fin )
22 21 anidms 
 |-  ( suc ( A u. B ) e. Fin -> ( suc ( A u. B ) X. suc ( A u. B ) ) e. Fin )
23 domfi 
 |-  ( ( ( suc ( A u. B ) X. suc ( A u. B ) ) e. Fin /\ ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) e. Fin )
24 22 23 sylan 
 |-  ( ( suc ( A u. B ) e. Fin /\ ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) e. Fin )
25 24 expcom 
 |-  ( ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) -> ( suc ( A u. B ) e. Fin -> ( _J0 ` <. A , B >. ) e. Fin ) )
26 20 25 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( suc ( A u. B ) e. Fin -> ( _J0 ` <. A , B >. ) e. Fin ) )
27 onenon 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( _J0 ` <. A , B >. ) e. dom card )
28 infinfnum 
 |-  ( ( _J0 ` <. A , B >. ) e. dom card -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) )
29 7 27 28 mp2b 
 |-  ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) )
30 29 biimpri 
 |-  ( _om ~<_ ( _J0 ` <. A , B >. ) -> -. ( _J0 ` <. A , B >. ) e. Fin )
31 26 30 nsyli 
 |-  ( ( A e. On /\ B e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> -. suc ( A u. B ) e. Fin ) )
32 onun2 
 |-  ( ( A e. On /\ B e. On ) -> ( A u. B ) e. On )
33 onsuc 
 |-  ( ( A u. B ) e. On -> suc ( A u. B ) e. On )
34 onenon 
 |-  ( suc ( A u. B ) e. On -> suc ( A u. B ) e. dom card )
35 32 33 34 3syl 
 |-  ( ( A e. On /\ B e. On ) -> suc ( A u. B ) e. dom card )
36 infinfnum 
 |-  ( suc ( A u. B ) e. dom card -> ( -. suc ( A u. B ) e. Fin <-> _om ~<_ suc ( A u. B ) ) )
37 35 36 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( -. suc ( A u. B ) e. Fin <-> _om ~<_ suc ( A u. B ) ) )
38 31 37 sylibd 
 |-  ( ( A e. On /\ B e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ suc ( A u. B ) ) )
39 19 38 syl 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ suc ( A u. B ) ) )
40 infxpidm2 
 |-  ( ( suc ( A u. B ) e. dom card /\ _om ~<_ suc ( A u. B ) ) -> ( suc ( A u. B ) X. suc ( A u. B ) ) ~~ suc ( A u. B ) )
41 35 40 sylan 
 |-  ( ( ( A e. On /\ B e. On ) /\ _om ~<_ suc ( A u. B ) ) -> ( suc ( A u. B ) X. suc ( A u. B ) ) ~~ suc ( A u. B ) )
42 41 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( suc ( A u. B ) X. suc ( A u. B ) ) ~~ suc ( A u. B ) ) )
43 domentr 
 |-  ( ( ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) /\ ( suc ( A u. B ) X. suc ( A u. B ) ) ~~ suc ( A u. B ) ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) )
44 20 42 43 syl6an 
 |-  ( ( A e. On /\ B e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) )
45 19 44 syl 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) ) )
46 onunel 
 |-  ( ( A e. On /\ B e. On /\ ( aleph ` C ) e. On ) -> ( ( A u. B ) e. ( aleph ` C ) <-> ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) ) )
47 15 46 mp3an3 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A u. B ) e. ( aleph ` C ) <-> ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) ) )
48 16 17 47 syl2an 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( ( A u. B ) e. ( aleph ` C ) <-> ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) ) )
49 48 ibir 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( A u. B ) e. ( aleph ` C ) )
50 49 3adant3 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( A u. B ) e. ( aleph ` C ) )
51 alephislim 
 |-  ( C e. On <-> Lim ( aleph ` C ) )
52 limsuc 
 |-  ( Lim ( aleph ` C ) -> ( ( A u. B ) e. ( aleph ` C ) <-> suc ( A u. B ) e. ( aleph ` C ) ) )
53 51 52 sylbi 
 |-  ( C e. On -> ( ( A u. B ) e. ( aleph ` C ) <-> suc ( A u. B ) e. ( aleph ` C ) ) )
54 53 3ad2ant3 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( A u. B ) e. ( aleph ` C ) <-> suc ( A u. B ) e. ( aleph ` C ) ) )
55 50 54 mpbid 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> suc ( A u. B ) e. ( aleph ` C ) )
56 18 32 33 3syl 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> suc ( A u. B ) e. On )
57 alephsdom 
 |-  ( ( suc ( A u. B ) e. On /\ C e. On ) -> ( suc ( A u. B ) e. ( aleph ` C ) <-> suc ( A u. B ) ~< ( aleph ` C ) ) )
58 56 57 stoic3 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( suc ( A u. B ) e. ( aleph ` C ) <-> suc ( A u. B ) ~< ( aleph ` C ) ) )
59 55 58 mpbid 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> suc ( A u. B ) ~< ( aleph ` C ) )
60 45 59 jctird 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) /\ suc ( A u. B ) ~< ( aleph ` C ) ) ) )
61 domsdomtr 
 |-  ( ( ( _J0 ` <. A , B >. ) ~<_ suc ( A u. B ) /\ suc ( A u. B ) ~< ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) )
62 60 61 syl6 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ suc ( A u. B ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) )
63 39 62 syld 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) )
64 alephsdom 
 |-  ( ( ( _J0 ` <. A , B >. ) e. On /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) )
65 7 64 mpan 
 |-  ( C e. On -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) )
66 65 3ad2ant3 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` C ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` C ) ) )
67 63 66 sylibrd 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) )
68 alephgeom 
 |-  ( C e. On <-> _om C_ ( aleph ` C ) )
69 68 biimpi 
 |-  ( C e. On -> _om C_ ( aleph ` C ) )
70 69 sselda 
 |-  ( ( C e. On /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) )
71 70 3ad2antl3 
 |-  ( ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) )
72 71 ex 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _J0 ` <. A , B >. ) e. _om -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) )
73 67 72 jaod 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( ( _om ~<_ ( _J0 ` <. A , B >. ) \/ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) )
74 14 73 mpi 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) /\ C e. On ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) )
75 74 3expia 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( C e. On -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) )
76 75 com12 
 |-  ( C e. On -> ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) )
77 alephfnon 
 |-  aleph Fn On
78 77 fndmi 
 |-  dom aleph = On
79 78 eleq2i 
 |-  ( C e. dom aleph <-> C e. On )
80 ndmfv 
 |-  ( -. C e. dom aleph -> ( aleph ` C ) = (/) )
81 79 80 sylnbir 
 |-  ( -. C e. On -> ( aleph ` C ) = (/) )
82 nel02 
 |-  ( ( aleph ` C ) = (/) -> -. A e. ( aleph ` C ) )
83 81 82 syl 
 |-  ( -. C e. On -> -. A e. ( aleph ` C ) )
84 83 intnanrd 
 |-  ( -. C e. On -> -. ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) )
85 84 pm2.21d 
 |-  ( -. C e. On -> ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) ) )
86 76 85 pm2.61i 
 |-  ( ( A e. ( aleph ` C ) /\ B e. ( aleph ` C ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` C ) )