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	⊢ ( 𝐴 ∈ On → 𝐴 = ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		jf1o	⊢ 𝐽 : ( ( On × On ) × 9o ) –1-1-onto→ On
2		f1ocnvdm	⊢ ( ( 𝐽 : ( ( On × On ) × 9o ) –1-1-onto→ On ∧ 𝐴 ∈ On ) → ( ◡ 𝐽 ‘ 𝐴 ) ∈ ( ( On × On ) × 9o ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ On → ( ◡ 𝐽 ‘ 𝐴 ) ∈ ( ( On × On ) × 9o ) )
4		2fveq3	⊢ ( 𝑥 = 𝐴 → ( 1st ‘ ( ◡ 𝐽 ‘ 𝑥 ) ) = ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) )
5	4	fveq2d	⊢ ( 𝑥 = 𝐴 → ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝑥 ) ) ) = ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) )
6		dfk12	⊢ 𝐾1 = ( 𝑥 ∈ On ↦ ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝑥 ) ) ) )
7		fvex	⊢ ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) ∈ V
8	5 6 7	fvmpt	⊢ ( 𝐴 ∈ On → ( 𝐾1 ‘ 𝐴 ) = ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) )
9	8	eqcomd	⊢ ( 𝐴 ∈ On → ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾1 ‘ 𝐴 ) )
10	4	fveq2d	⊢ ( 𝑥 = 𝐴 → ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝑥 ) ) ) = ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) )
11		dfk22	⊢ 𝐾2 = ( 𝑥 ∈ On ↦ ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝑥 ) ) ) )
12		fvex	⊢ ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) ∈ V
13	10 11 12	fvmpt	⊢ ( 𝐴 ∈ On → ( 𝐾2 ‘ 𝐴 ) = ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) )
14	13	eqcomd	⊢ ( 𝐴 ∈ On → ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾2 ‘ 𝐴 ) )
15		2fveq3	⊢ ( 𝑥 = 𝐴 → ( 2nd ‘ ( ◡ 𝐽 ‘ 𝑥 ) ) = ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) )
16		dfk32	⊢ 𝐾3 = ( 𝑥 ∈ On ↦ ( 2nd ‘ ( ◡ 𝐽 ‘ 𝑥 ) ) )
17		fvex	⊢ ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ∈ V
18	15 16 17	fvmpt	⊢ ( 𝐴 ∈ On → ( 𝐾3 ‘ 𝐴 ) = ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) )
19	18	eqcomd	⊢ ( 𝐴 ∈ On → ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) = ( 𝐾3 ‘ 𝐴 ) )
20	9 14 19	3jca	⊢ ( 𝐴 ∈ On → ( ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾1 ‘ 𝐴 ) ∧ ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾2 ‘ 𝐴 ) ∧ ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) = ( 𝐾3 ‘ 𝐴 ) ) )
21	3 20	jca	⊢ ( 𝐴 ∈ On → ( ( ◡ 𝐽 ‘ 𝐴 ) ∈ ( ( On × On ) × 9o ) ∧ ( ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾1 ‘ 𝐴 ) ∧ ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾2 ‘ 𝐴 ) ∧ ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) = ( 𝐾3 ‘ 𝐴 ) ) ) )
22		k1on	⊢ ( 𝐾1 ‘ 𝐴 ) ∈ On
23		k2on	⊢ ( 𝐾2 ‘ 𝐴 ) ∈ On
24		k39o	⊢ ( 𝐾3 ‘ 𝐴 ) ∈ 9o
25		el2xptp0	⊢ ( ( ( 𝐾1 ‘ 𝐴 ) ∈ On ∧ ( 𝐾2 ‘ 𝐴 ) ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ∈ 9o ) → ( ( ( ◡ 𝐽 ‘ 𝐴 ) ∈ ( ( On × On ) × 9o ) ∧ ( ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾1 ‘ 𝐴 ) ∧ ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾2 ‘ 𝐴 ) ∧ ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) = ( 𝐾3 ‘ 𝐴 ) ) ) ↔ ( ◡ 𝐽 ‘ 𝐴 ) = ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) )
26	22 23 24 25	mp3an	⊢ ( ( ( ◡ 𝐽 ‘ 𝐴 ) ∈ ( ( On × On ) × 9o ) ∧ ( ( 1st ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾1 ‘ 𝐴 ) ∧ ( 2nd ‘ ( 1st ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) ) = ( 𝐾2 ‘ 𝐴 ) ∧ ( 2nd ‘ ( ◡ 𝐽 ‘ 𝐴 ) ) = ( 𝐾3 ‘ 𝐴 ) ) ) ↔ ( ◡ 𝐽 ‘ 𝐴 ) = ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ )
27	21 26	sylib	⊢ ( 𝐴 ∈ On → ( ◡ 𝐽 ‘ 𝐴 ) = ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ )
28	27 3	eqeltrrd	⊢ ( 𝐴 ∈ On → ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ∈ ( ( On × On ) × 9o ) )
29		f1ocnvfvb	⊢ ( ( 𝐽 : ( ( On × On ) × 9o ) –1-1-onto→ On ∧ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ∈ ( ( On × On ) × 9o ) ∧ 𝐴 ∈ On ) → ( ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) = 𝐴 ↔ ( ◡ 𝐽 ‘ 𝐴 ) = ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) )
30	1 29	mp3an1	⊢ ( ( ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ∈ ( ( On × On ) × 9o ) ∧ 𝐴 ∈ On ) → ( ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) = 𝐴 ↔ ( ◡ 𝐽 ‘ 𝐴 ) = ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) )
31	28 30	mpancom	⊢ ( 𝐴 ∈ On → ( ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) = 𝐴 ↔ ( ◡ 𝐽 ‘ 𝐴 ) = ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) )
32	27 31	mpbird	⊢ ( 𝐴 ∈ On → ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) = 𝐴 )
33	32	eqcomd	⊢ ( 𝐴 ∈ On → 𝐴 = ( 𝐽 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) , ( 𝐾3 ‘ 𝐴 ) ⟩ ) )