Metamath Proof Explorer

Theorem jf1

Description: _J is a one-to-one function. Part of Proposition 15.3 of TakeutiZaring p. 155. (Contributed by BTernaryTau, 6-Oct-2026)

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

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 2 3 ax-mp 
 |-  _J0 : ( On X. On ) -1-1-onto-> On
5 f1of 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On )
6 4 5 ax-mp 
 |-  _J0 : ( On X. On ) --> On
7 0elon 
 |-  (/) e. On
8 6 7 f0cli 
 |-  ( _J0 ` ( 1st ` w ) ) e. On
9 omcl 
 |-  ( ( 9o e. On /\ ( _J0 ` ( 1st ` w ) ) e. On ) -> ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On )
10 1 8 9 mp2an 
 |-  ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On
11 xp2nd 
 |-  ( w e. ( ( On X. On ) X. 9o ) -> ( 2nd ` w ) e. 9o )
12 onelon 
 |-  ( ( 9o e. On /\ ( 2nd ` w ) e. 9o ) -> ( 2nd ` w ) e. On )
13 1 11 12 sylancr 
 |-  ( w e. ( ( On X. On ) X. 9o ) -> ( 2nd ` w ) e. On )
14 oacl 
 |-  ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On /\ ( 2nd ` w ) e. On ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On )
15 10 13 14 sylancr 
 |-  ( w e. ( ( On X. On ) X. 9o ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On )
16 15 rgen 
 |-  A. w e. ( ( On X. On ) X. 9o ) ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On
17 1 a1i 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> 9o e. On )
18 df-9o 
 |-  9o = suc 8o
19 nsuceq0 
 |-  suc 8o =/= (/)
20 18 19 eqnetri 
 |-  9o =/= (/)
21 20 a1i 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> 9o =/= (/) )
22 8 a1i 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( _J0 ` ( 1st ` w ) ) e. On )
23 11 3ad2ant1 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( 2nd ` w ) e. 9o )
24 6 7 f0cli 
 |-  ( _J0 ` ( 1st ` z ) ) e. On
25 24 a1i 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( _J0 ` ( 1st ` z ) ) e. On )
26 xp2nd 
 |-  ( z e. ( ( On X. On ) X. 9o ) -> ( 2nd ` z ) e. 9o )
27 26 3ad2ant2 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( 2nd ` z ) e. 9o )
28 simp3 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) )
29 17 21 22 23 25 27 28 omeueq 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) )
30 xp1st 
 |-  ( w e. ( ( On X. On ) X. 9o ) -> ( 1st ` w ) e. ( On X. On ) )
31 xp1st 
 |-  ( z e. ( ( On X. On ) X. 9o ) -> ( 1st ` z ) e. ( On X. On ) )
32 f1of1 
 |-  ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) -1-1-> On )
33 4 32 ax-mp 
 |-  _J0 : ( On X. On ) -1-1-> On
34 f1veqaeq 
 |-  ( ( _J0 : ( On X. On ) -1-1-> On /\ ( ( 1st ` w ) e. ( On X. On ) /\ ( 1st ` z ) e. ( On X. On ) ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) )
35 33 34 mpan 
 |-  ( ( ( 1st ` w ) e. ( On X. On ) /\ ( 1st ` z ) e. ( On X. On ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) )
36 30 31 35 syl2an 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) )
37 36 anim1d 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) )
38 37 3adant3 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) )
39 29 38 mpd 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) )
40 xpopth 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) <-> w = z ) )
41 40 3adant3 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) <-> w = z ) )
42 39 41 mpbid 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> w = z )
43 42 3expia 
 |-  ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) )
44 43 rgen2 
 |-  A. w e. ( ( On X. On ) X. 9o ) A. z e. ( ( On X. On ) X. 9o ) ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z )
45 dfj2 
 |-  _J = ( w e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) )
46 2fveq3 
 |-  ( w = z -> ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) )
47 46 oveq2d 
 |-  ( w = z -> ( 9o .o ( _J0 ` ( 1st ` w ) ) ) = ( 9o .o ( _J0 ` ( 1st ` z ) ) ) )
48 fveq2 
 |-  ( w = z -> ( 2nd ` w ) = ( 2nd ` z ) )
49 47 48 oveq12d 
 |-  ( w = z -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) )
50 45 49 f1mpt 
 |-  ( _J : ( ( On X. On ) X. 9o ) -1-1-> On <-> ( A. w e. ( ( On X. On ) X. 9o ) ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On /\ A. w e. ( ( On X. On ) X. 9o ) A. z e. ( ( On X. On ) X. 9o ) ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) ) )
51 16 44 50 mpbir2an 
 |-  _J : ( ( On X. On ) X. 9o ) -1-1-> On