dfk12

Description: Alternate definition of _K1 using maps-to notation. (Contributed by BTernaryTau, 9-Oct-2026)

		Ref	Expression
	Assertion	dfk12	⊢ 𝐾₁ = ( 𝑥 ∈ On ↦ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) → 𝑥 ∈ On )
2		simpllr	⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) ∧ 𝑦 ∈ On ) → 𝑧 ∈ On )
3		simpr	⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) ∧ 𝑦 ∈ On ) → 𝑦 ∈ On )
4		simplr	⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) ∧ 𝑦 ∈ On ) → 𝑛 ∈ 9_o )
5		simplll	⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) ∧ 𝑦 ∈ On ) → 𝑥 ∈ On )
6		eqcom	⊢ ( 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ↔ ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) = 𝑥 )
7		otelxp	⊢ ( ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ∈ ( ( On × On ) × 9_o ) ↔ ( 𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o ) )
8		jf1o	⊢ 𝐽 : ( ( On × On ) × 9_o ) –1-1-onto→ On
9		f1ocnvfvb	⊢ ( ( 𝐽 : ( ( On × On ) × 9_o ) –1-1-onto→ On ∧ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ∈ ( ( On × On ) × 9_o ) ∧ 𝑥 ∈ On ) → ( ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) = 𝑥 ↔ ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) )
10	8 9	mp3an1	⊢ ( ( ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ∈ ( ( On × On ) × 9_o ) ∧ 𝑥 ∈ On ) → ( ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) = 𝑥 ↔ ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) )
11	7 10	sylanbr	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o ) ∧ 𝑥 ∈ On ) → ( ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) = 𝑥 ↔ ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) )
12		vex	⊢ 𝑧 ∈ V
13		vex	⊢ 𝑦 ∈ V
14		vex	⊢ 𝑛 ∈ V
15	12 13 14	3pm3.2i	⊢ ( 𝑧 ∈ V ∧ 𝑦 ∈ V ∧ 𝑛 ∈ V )
16		oteqimp	⊢ ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → ( ( 𝑧 ∈ V ∧ 𝑦 ∈ V ∧ 𝑛 ∈ V ) → ( ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) = 𝑧 ∧ ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) = 𝑦 ∧ ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) = 𝑛 ) ) )
17	15 16	mpi	⊢ ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → ( ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) = 𝑧 ∧ ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) = 𝑦 ∧ ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) = 𝑛 ) )
18	17	simp1d	⊢ ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) = 𝑧 )
19	18	eqcomd	⊢ ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) )
20	11 19	biimtrdi	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o ) ∧ 𝑥 ∈ On ) → ( ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) = 𝑥 → 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) )
21	6 20	biimtrid	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o ) ∧ 𝑥 ∈ On ) → ( 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) )
22	2 3 4 5 21	syl31anc	⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) ∧ 𝑦 ∈ On ) → ( 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) )
23	22	rexlimdva	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) → ( ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) )
24	23	rexlimdva	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) )
25	24	impr	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) → 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) )
26	1 25	jca	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) → ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) )
27		f1ocnvdm	⊢ ( ( 𝐽 : ( ( On × On ) × 9_o ) –1-1-onto→ On ∧ 𝑥 ∈ On ) → ( ^◡ 𝐽 ‘ 𝑥 ) ∈ ( ( On × On ) × 9_o ) )
28	8 27	mpan	⊢ ( 𝑥 ∈ On → ( ^◡ 𝐽 ‘ 𝑥 ) ∈ ( ( On × On ) × 9_o ) )
29		xp1st	⊢ ( ( ^◡ 𝐽 ‘ 𝑥 ) ∈ ( ( On × On ) × 9_o ) → ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ∈ ( On × On ) )
30		xp1st	⊢ ( ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ∈ ( On × On ) → ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On )
31	28 29 30	3syl	⊢ ( 𝑥 ∈ On → ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On )
32	31	adantr	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On )
33		eleq1	⊢ ( 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) → ( 𝑧 ∈ On ↔ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On ) )
34	33	adantl	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( 𝑧 ∈ On ↔ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On ) )
35	32 34	mpbird	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → 𝑧 ∈ On )
36		oteq3	⊢ ( 𝑛 = ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) → ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ = ⟨ 𝑧 , 𝑦 , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
37	36	eqeq2d	⊢ ( 𝑛 = ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) → ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ↔ ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ ) )
38		oteq2	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) → ⟨ 𝑧 , 𝑦 , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ = ⟨ 𝑧 , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
39	38	eqeq2d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) → ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ ↔ ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ ) )
40		xp2nd	⊢ ( ( ^◡ 𝐽 ‘ 𝑥 ) ∈ ( ( On × On ) × 9_o ) → ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ∈ 9_o )
41	28 40	syl	⊢ ( 𝑥 ∈ On → ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ∈ 9_o )
42	41	adantr	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ∈ 9_o )
43		xp2nd	⊢ ( ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ∈ ( On × On ) → ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On )
44	28 29 43	3syl	⊢ ( 𝑥 ∈ On → ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On )
45	44	adantr	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ∈ On )
46		ot1st2nd	⊢ ( ( ^◡ 𝐽 ‘ 𝑥 ) ∈ ( ( On × On ) × 9_o ) → ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
47	28 46	syl	⊢ ( 𝑥 ∈ On → ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
48	47	adantr	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
49		oteq1	⊢ ( 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) → ⟨ 𝑧 , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ = ⟨ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
50	49	adantl	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ⟨ 𝑧 , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ = ⟨ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
51	48 50	eqtr4d	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , ( 2^nd ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) , ( 2^nd ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ⟩ )
52	37 39 42 45 51	2rspcedvdw	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ )
53	11	biimprd	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o ) ∧ 𝑥 ∈ On ) → ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) = 𝑥 ) )
54	53 6	imbitrrdi	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o ) ∧ 𝑥 ∈ On ) → ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) )
55	2 3 4 5 54	syl31anc	⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) ∧ 𝑦 ∈ On ) → ( ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) )
56	55	reximdva	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) ∧ 𝑛 ∈ 9_o ) → ( ∃ 𝑦 ∈ On ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) )
57	56	reximdva	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) )
58	35 57	syldan	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On ( ^◡ 𝐽 ‘ 𝑥 ) = ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ → ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) )
59	52 58	mpd	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) )
60	35 59	jca	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) )
61		f1of	⊢ ( 𝐽 : ( ( On × On ) × 9_o ) –1-1-onto→ On → 𝐽 : ( ( On × On ) × 9_o ) ⟶ On )
62	8 61	ax-mp	⊢ 𝐽 : ( ( On × On ) × 9_o ) ⟶ On
63		0elon	⊢ ∅ ∈ On
64	62 63	f0cli	⊢ ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ∈ On
65		eleq1	⊢ ( 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → ( 𝑥 ∈ On ↔ ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ∈ On ) )
66	64 65	mpbiri	⊢ ( 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → 𝑥 ∈ On )
67	66	rexlimivw	⊢ ( ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → 𝑥 ∈ On )
68	67	rexlimivw	⊢ ( ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) → 𝑥 ∈ On )
69	68	adantl	⊢ ( ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) → 𝑥 ∈ On )
70	60 69	jccil	⊢ ( ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) → ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) )
71	26 70	impbii	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) ↔ ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) )
72	71	opabbii	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) }
73		df-k1	⊢ 𝐾₁ = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) }
74	69	pm4.71ri	⊢ ( ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ↔ ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) )
75	74	opabbii	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) }
76	73 75	eqtri	⊢ 𝐾₁ = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ On ∧ ( 𝑧 ∈ On ∧ ∃ 𝑛 ∈ 9_o ∃ 𝑦 ∈ On 𝑥 = ( 𝐽 ‘ ⟨ 𝑧 , 𝑦 , 𝑛 ⟩ ) ) ) }
77		df-mpt	⊢ ( 𝑥 ∈ On ↦ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ On ∧ 𝑧 = ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) ) }
78	72 76 77	3eqtr4i	⊢ 𝐾₁ = ( 𝑥 ∈ On ↦ ( 1^st ‘ ( 1^st ‘ ( ^◡ 𝐽 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem dfk12

Proof