Metamath Proof Explorer

Theorem jk1k2k3

Description: Identity law for the _J function. Proposition 15.8 of TakeutiZaring p. 156. (Contributed by BTernaryTau, 11-Oct-2026)

Ref Expression
Assertion jk1k2k3 
|- ( A e. On -> A = ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) )

Proof

Step Hyp Ref Expression
1 jf1o 
 |-  _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On
2 f1ocnvdm 
 |-  ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ A e. On ) -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) )
3 1 2 mpan 
 |-  ( A e. On -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) )
4 2fveq3 
 |-  ( x = A -> ( 1st ` ( `' _J ` x ) ) = ( 1st ` ( `' _J ` A ) ) )
5 4 fveq2d 
 |-  ( x = A -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) )
6 dfk12 
 |-  _K1 = ( x e. On |-> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) )
7 fvex 
 |-  ( 1st ` ( 1st ` ( `' _J ` A ) ) ) e. _V
8 5 6 7 fvmpt 
 |-  ( A e. On -> ( _K1 ` A ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) )
9 8 eqcomd 
 |-  ( A e. On -> ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) )
10 4 fveq2d 
 |-  ( x = A -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) )
11 dfk22 
 |-  _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) )
12 fvex 
 |-  ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. _V
13 10 11 12 fvmpt 
 |-  ( A e. On -> ( _K2 ` A ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) )
14 13 eqcomd 
 |-  ( A e. On -> ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) )
15 2fveq3 
 |-  ( x = A -> ( 2nd ` ( `' _J ` x ) ) = ( 2nd ` ( `' _J ` A ) ) )
16 dfk32 
 |-  _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) )
17 fvex 
 |-  ( 2nd ` ( `' _J ` A ) ) e. _V
18 15 16 17 fvmpt 
 |-  ( A e. On -> ( _K3 ` A ) = ( 2nd ` ( `' _J ` A ) ) )
19 18 eqcomd 
 |-  ( A e. On -> ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) )
20 9 14 19 3jca 
 |-  ( A e. On -> ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) )
21 3 20 jca 
 |-  ( A e. On -> ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) )
22 k1on 
 |-  ( _K1 ` A ) e. On
23 k2on 
 |-  ( _K2 ` A ) e. On
24 k39o 
 |-  ( _K3 ` A ) e. 9o
25 el2xptp0 
 |-  ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On /\ ( _K3 ` A ) e. 9o ) -> ( ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) )
26 22 23 24 25 mp3an 
 |-  ( ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. )
27 21 26 sylib 
 |-  ( A e. On -> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. )
28 27 3 eqeltrrd 
 |-  ( A e. On -> <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) )
29 f1ocnvfvb 
 |-  ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) /\ A e. On ) -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) )
30 1 29 mp3an1 
 |-  ( ( <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) /\ A e. On ) -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) )
31 28 30 mpancom 
 |-  ( A e. On -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) )
32 27 31 mpbird 
 |-  ( A e. On -> ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A )
33 32 eqcomd 
 |-  ( A e. On -> A = ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) )