Metamath Proof Explorer

Theorem jf1o

Description: _J is a bijection from ( ( On X. On ) X. 9o ) to On . Proposition 15.3 of TakeutiZaring p. 155. (Contributed by BTernaryTau, 6-Oct-2026)

Ref Expression
Assertion jf1o 
|- _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On

Proof

Step Hyp Ref Expression
1 jf1 
 |-  _J : ( ( On X. On ) X. 9o ) -1-1-> On
2 f1f 
 |-  ( _J : ( ( On X. On ) X. 9o ) -1-1-> On -> _J : ( ( On X. On ) X. 9o ) --> On )
3 frn 
 |-  ( _J : ( ( On X. On ) X. 9o ) --> On -> ran _J C_ On )
4 1 2 3 mp2b 
 |-  ran _J C_ On
5 ssab 
 |-  ( On C_ { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) } <-> A. w ( w e. On -> E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) )
6 9on 
 |-  9o e. On
7 df-9o 
 |-  9o = suc 8o
8 nsuceq0 
 |-  suc 8o =/= (/)
9 7 8 eqnetri 
 |-  9o =/= (/)
10 omeulem1 
 |-  ( ( 9o e. On /\ w e. On /\ 9o =/= (/) ) -> E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w )
11 6 9 10 mp3an13 
 |-  ( w e. On -> E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w )
12 j0iso 
 |-  _J0 Isom _R0 , _E ( ( On X. On ) , On )
13 isof1o 
 |-  ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On )
14 f1ofo 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) -onto-> On )
15 12 13 14 mp2b 
 |-  _J0 : ( On X. On ) -onto-> On
16 foelcdmi 
 |-  ( ( _J0 : ( On X. On ) -onto-> On /\ t e. On ) -> E. u e. ( On X. On ) ( _J0 ` u ) = t )
17 15 16 mpan 
 |-  ( t e. On -> E. u e. ( On X. On ) ( _J0 ` u ) = t )
18 oveq2 
 |-  ( ( _J0 ` u ) = t -> ( 9o .o ( _J0 ` u ) ) = ( 9o .o t ) )
19 18 oveq1d 
 |-  ( ( _J0 ` u ) = t -> ( ( 9o .o ( _J0 ` u ) ) +o v ) = ( ( 9o .o t ) +o v ) )
20 19 eqeq2d 
 |-  ( ( _J0 ` u ) = t -> ( w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> w = ( ( 9o .o t ) +o v ) ) )
21 eqcom 
 |-  ( w = ( ( 9o .o t ) +o v ) <-> ( ( 9o .o t ) +o v ) = w )
22 20 21 bitrdi 
 |-  ( ( _J0 ` u ) = t -> ( w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> ( ( 9o .o t ) +o v ) = w ) )
23 22 rexbidv 
 |-  ( ( _J0 ` u ) = t -> ( E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> E. v e. 9o ( ( 9o .o t ) +o v ) = w ) )
24 23 biimprcd 
 |-  ( E. v e. 9o ( ( 9o .o t ) +o v ) = w -> ( ( _J0 ` u ) = t -> E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) )
25 24 reximdv 
 |-  ( E. v e. 9o ( ( 9o .o t ) +o v ) = w -> ( E. u e. ( On X. On ) ( _J0 ` u ) = t -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) )
26 17 25 mpan9 
 |-  ( ( t e. On /\ E. v e. 9o ( ( 9o .o t ) +o v ) = w ) -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) )
27 26 rexlimiva 
 |-  ( E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) )
28 11 27 syl 
 |-  ( w e. On -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) )
29 vex 
 |-  u e. _V
30 vex 
 |-  v e. _V
31 29 30 op1std 
 |-  ( z = <. u , v >. -> ( 1st ` z ) = u )
32 31 fveq2d 
 |-  ( z = <. u , v >. -> ( _J0 ` ( 1st ` z ) ) = ( _J0 ` u ) )
33 32 oveq2d 
 |-  ( z = <. u , v >. -> ( 9o .o ( _J0 ` ( 1st ` z ) ) ) = ( 9o .o ( _J0 ` u ) ) )
34 29 30 op2ndd 
 |-  ( z = <. u , v >. -> ( 2nd ` z ) = v )
35 33 34 oveq12d 
 |-  ( z = <. u , v >. -> ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) = ( ( 9o .o ( _J0 ` u ) ) +o v ) )
36 35 eqeq2d 
 |-  ( z = <. u , v >. -> ( w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) <-> w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) )
37 36 rexxp 
 |-  ( E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) <-> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) )
38 28 37 sylibr 
 |-  ( w e. On -> E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) )
39 5 38 mpgbir 
 |-  On C_ { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) }
40 dfj2 
 |-  _J = ( z e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) )
41 40 rnmpt 
 |-  ran _J = { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) }
42 39 41 sseqtrri 
 |-  On C_ ran _J
43 4 42 eqssi 
 |-  ran _J = On
44 dff1o5 
 |-  ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On <-> ( _J : ( ( On X. On ) X. 9o ) -1-1-> On /\ ran _J = On ) )
45 1 43 44 mpbir2an 
 |-  _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On