Metamath Proof Explorer

Theorem jltaleph

Description: The value of _J is less than an aleph if its first two arguments are less than that aleph. Proposition 15.11 of TakeutiZaring p. 156. (Contributed by BTernaryTau, 16-Oct-2026)

Ref Expression
Assertion jltaleph 
|- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) )

Proof

Step Hyp Ref Expression
1 alephon 
 |-  ( aleph ` D ) e. On
2 1 oneli 
 |-  ( A e. ( aleph ` D ) -> A e. On )
3 2 3ad2ant1 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> A e. On )
4 1 oneli 
 |-  ( B e. ( aleph ` D ) -> B e. On )
5 4 3ad2ant2 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> B e. On )
6 simp3 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> C e. 9o )
7 ovexd 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _V )
8 opeq1 
 |-  ( A = x -> <. A , y >. = <. x , y >. )
9 8 fveq2d 
 |-  ( A = x -> ( _J0 ` <. A , y >. ) = ( _J0 ` <. x , y >. ) )
10 9 oveq2d 
 |-  ( A = x -> ( 9o .o ( _J0 ` <. A , y >. ) ) = ( 9o .o ( _J0 ` <. x , y >. ) ) )
11 10 oveq1d 
 |-  ( A = x -> ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )
12 11 adantl 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ A = x ) -> ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )
13 opeq2 
 |-  ( B = y -> <. A , B >. = <. A , y >. )
14 13 fveq2d 
 |-  ( B = y -> ( _J0 ` <. A , B >. ) = ( _J0 ` <. A , y >. ) )
15 14 oveq2d 
 |-  ( B = y -> ( 9o .o ( _J0 ` <. A , B >. ) ) = ( 9o .o ( _J0 ` <. A , y >. ) ) )
16 15 oveq1d 
 |-  ( B = y -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) )
17 16 adantl 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ B = y ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) )
18 oveq2 
 |-  ( C = n -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) )
19 18 adantl 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ C = n ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) )
20 df-j 
 |-  _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) )
21 3 5 6 7 12 17 19 20 mpt3fvot2d 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) )
22 21 adantr 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) )
23 6 anim1ci 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) )
24 alephfnon 
 |-  aleph Fn On
25 24 fndmi 
 |-  dom aleph = On
26 25 eleq2i 
 |-  ( D e. dom aleph <-> D e. On )
27 ndmfv 
 |-  ( -. D e. dom aleph -> ( aleph ` D ) = (/) )
28 26 27 sylnbir 
 |-  ( -. D e. On -> ( aleph ` D ) = (/) )
29 nel02 
 |-  ( ( aleph ` D ) = (/) -> -. A e. ( aleph ` D ) )
30 28 29 syl 
 |-  ( -. D e. On -> -. A e. ( aleph ` D ) )
31 30 con4i 
 |-  ( A e. ( aleph ` D ) -> D e. On )
32 31 3ad2ant1 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> D e. On )
33 32 adantr 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> D e. On )
34 alephgeom 
 |-  ( D e. On <-> _om C_ ( aleph ` D ) )
35 34 bilani 
 |-  ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> _om C_ ( aleph ` D ) )
36 9onn 
 |-  9o e. _om
37 nnmcl 
 |-  ( ( 9o e. _om /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om )
38 36 37 mpan 
 |-  ( ( _J0 ` <. A , B >. ) e. _om -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om )
39 elnn 
 |-  ( ( C e. 9o /\ 9o e. _om ) -> C e. _om )
40 36 39 mpan2 
 |-  ( C e. 9o -> C e. _om )
41 nnacl 
 |-  ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om /\ C e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om )
42 38 40 41 syl2an 
 |-  ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om )
43 42 adantr 
 |-  ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om )
44 35 43 sseldd 
 |-  ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. ( aleph ` D ) )
45 23 33 44 syl2anc 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. ( aleph ` D ) )
46 22 45 eqeltrd 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) )
47 21 adantr 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) )
48 j0iso 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )
49 isof1o 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On )
50 f1of 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On )
51 48 49 50 mp2b 
 |-  _J0 : ( On X. On ) --> On
52 0elon 
 |-  (/) e. On
53 51 52 f0cli 
 |-  ( _J0 ` <. A , B >. ) e. On
54 onfin 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( ( _J0 ` <. A , B >. ) e. Fin <-> ( _J0 ` <. A , B >. ) e. _om ) )
55 54 notbid 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> -. ( _J0 ` <. A , B >. ) e. _om ) )
56 onenon 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( _J0 ` <. A , B >. ) e. dom card )
57 infinfnum 
 |-  ( ( _J0 ` <. A , B >. ) e. dom card -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) )
58 56 57 syl 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) )
59 55 58 bitr3d 
 |-  ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. _om <-> _om ~<_ ( _J0 ` <. A , B >. ) ) )
60 53 59 ax-mp 
 |-  ( -. ( _J0 ` <. A , B >. ) e. _om <-> _om ~<_ ( _J0 ` <. A , B >. ) )
61 jltalephlem 
 |-  ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) )
62 60 61 sylan2b 
 |-  ( ( C e. 9o /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) )
63 62 3ad2antl3 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) )
64 47 63 eqbrtrd 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) ~~ ( _J0 ` <. A , B >. ) )
65 j0ltaleph 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` D ) )
66 alephsdom 
 |-  ( ( ( _J0 ` <. A , B >. ) e. On /\ D e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) )
67 53 31 66 sylancr 
 |-  ( A e. ( aleph ` D ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) )
68 67 adantr 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) )
69 65 68 mpbid 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) )
70 69 3adant3 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) )
71 70 adantr 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) )
72 ensdomtr 
 |-  ( ( ( _J ` <. A , B , C >. ) ~~ ( _J0 ` <. A , B >. ) /\ ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) -> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) )
73 64 71 72 syl2anc 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) )
74 jf1 
 |-  _J : ( ( On X. On ) X. 9o ) -1-1-> On
75 f1f 
 |-  ( _J : ( ( On X. On ) X. 9o ) -1-1-> On -> _J : ( ( On X. On ) X. 9o ) --> On )
76 74 75 ax-mp 
 |-  _J : ( ( On X. On ) X. 9o ) --> On
77 76 52 f0cli 
 |-  ( _J ` <. A , B , C >. ) e. On
78 alephsdom 
 |-  ( ( ( _J ` <. A , B , C >. ) e. On /\ D e. On ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) )
79 77 31 78 sylancr 
 |-  ( A e. ( aleph ` D ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) )
80 79 3ad2ant1 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) )
81 80 adantr 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) )
82 73 81 mpbird 
 |-  ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) )
83 46 82 pm2.61dan 
 |-  ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) )