curf2cl

Description: The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curf2.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
	curf2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	curf2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	curf2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	curf2.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
	curf2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	curf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	curf2.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
	curf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	curf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	curf2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
	curf2.l	⊢ 𝐿 = ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 )
	curf2.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
Assertion	curf2cl	⊢ ( 𝜑 → 𝐿 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		curf2.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
2		curf2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		curf2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		curf2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		curf2.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
6		curf2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		curf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
8		curf2.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
9		curf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
10		curf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
11		curf2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
12		curf2.l	⊢ 𝐿 = ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 )
13		curf2.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
14	1 2 3 4 5 6 7 8 9 10 11 12	curf2	⊢ ( 𝜑 → 𝐿 = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )
15		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
16	15 2 6	xpcbas	⊢ ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
17		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
18		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
19		relfunc	⊢ Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 )
20		1st2ndbr	⊢ ( ( Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ∧ 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
21	19 5 20	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
23		opelxpi	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
24	9 23	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
25		opelxpi	⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝑌 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
26	10 25	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝑌 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
27	16 17 18 22 24 26	funcf2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) : ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑧 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ) )
28		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
29	9	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
31	10	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑌 ∈ 𝐴 )
32	15 2 6 7 28 29 30 31 30 17	xpchom2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑧 ⟩ ) = ( ( 𝑋 𝐻 𝑌 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
33	32	feq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) : ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑧 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ) ↔ ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) : ( ( 𝑋 𝐻 𝑌 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ) ) )
34	27 33	mpbid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) : ( ( 𝑋 𝐻 𝑌 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ) )
35	11	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
36	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐷 ∈ Cat )
37	6 28 8 36 30	catidcl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑧 ) ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) )
38	34 35 37	fovrnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ) )
39	3	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐶 ∈ Cat )
40	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
41		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 )
42	1 2 39 36 40 6 29 41 30	curf11	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑧 ) )
43		df-ov	⊢ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ )
44	42 43	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) )
45		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 )
46	1 2 39 36 40 6 31 45 30	curf11	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) = ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑧 ) )
47		df-ov	⊢ ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ )
48	46 47	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) )
49	44 48	oveq12d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ) )
50	38 49	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
51	50	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
52	6	fvexi	⊢ 𝐵 ∈ V
53		mptelixpg	⊢ ( 𝐵 ∈ V → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) ) )
54	52 53	ax-mp	⊢ ( ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
55	51 54	sylibr	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
56	14 55	eqeltrd	⊢ ( 𝜑 → 𝐿 ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
57		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
58	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
59	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑋 ∈ 𝐴 )
60		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
61	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑌 ∈ 𝐴 )
62	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
63	2 7 57 58 59 60 61 62	catrid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐾 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = 𝐾 )
64	2 7 57 58 59 60 61 62	catlid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐾 ) = 𝐾 )
65	63 64	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐾 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐾 ) )
66	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐷 ∈ Cat )
67		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑧 ∈ 𝐵 )
68		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
69		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑤 ∈ 𝐵 )
70		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) )
71	6 28 8 66 67 68 69 70	catlid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝐼 ‘ 𝑤 ) ( ⟨ 𝑧 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑓 ) = 𝑓 )
72	6 28 8 66 67 68 69 70	catrid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) ( 𝐼 ‘ 𝑧 ) ) = 𝑓 )
73	71 72	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝐼 ‘ 𝑤 ) ( ⟨ 𝑧 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) ( 𝐼 ‘ 𝑧 ) ) )
74	65 73	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( 𝐾 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) , ( ( 𝐼 ‘ 𝑤 ) ( ⟨ 𝑧 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑓 ) ⟩ = ⟨ ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐾 ) , ( 𝑓 ( ⟨ 𝑧 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) ( 𝐼 ‘ 𝑧 ) ) ⟩ )
75		eqid	⊢ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) = ( comp ‘ ( 𝐶 ×_c 𝐷 ) )
76	2 7 57 58 59	catidcl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
77	6 28 8 66 69	catidcl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐼 ‘ 𝑤 ) ∈ ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) )
78	15 2 6 7 28 59 67 59 69 60 68 75 61 69 76 70 62 77	xpcco2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑋 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) , ( ( 𝐼 ‘ 𝑤 ) ( ⟨ 𝑧 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑓 ) ⟩ )
79	37	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐼 ‘ 𝑧 ) ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) )
80	2 7 57 58 61	catidcl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ∈ ( 𝑌 𝐻 𝑌 ) )
81	15 2 6 7 28 59 67 61 67 60 68 75 61 69 62 79 80 70	xpcco2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑌 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) = ⟨ ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐾 ) , ( 𝑓 ( ⟨ 𝑧 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) ( 𝐼 ‘ 𝑧 ) ) ⟩ )
82	74 78 81	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑋 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) = ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑌 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) )
83	82	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ( ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑋 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) ) = ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑌 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) ) )
84		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
85	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
86	24	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑋 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
87	59 69	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑋 , 𝑤 ⟩ ∈ ( 𝐴 × 𝐵 ) )
88	61 69	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑌 , 𝑤 ⟩ ∈ ( 𝐴 × 𝐵 ) )
89	76 70	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ∈ ( ( 𝑋 𝐻 𝑋 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
90	15 2 6 7 28 59 67 59 69 17	xpchom2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) = ( ( 𝑋 𝐻 𝑋 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
91	89 90	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ∈ ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) )
92	62 77	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ∈ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
93	15 2 6 7 28 59 69 61 69 17	xpchom2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑋 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) = ( ( 𝑋 𝐻 𝑌 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
94	92 93	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ∈ ( ⟨ 𝑋 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) )
95	16 17 75 84 85 86 87 88 91 94	funcco	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ( ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑋 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) ) = ( ( ( ⟨ 𝑋 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) ) )
96	26	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑌 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
97	62 79	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ∈ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
98	15 2 6 7 28 59 67 61 67 17	xpchom2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑧 ⟩ ) = ( ( 𝑋 𝐻 𝑌 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
99	97 98	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ∈ ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑧 ⟩ ) )
100	80 70	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ∈ ( ( 𝑌 𝐻 𝑌 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
101	15 2 6 7 28 61 67 61 69 17	xpchom2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑌 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) = ( ( 𝑌 𝐻 𝑌 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
102	100 101	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ∈ ( ⟨ 𝑌 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) )
103	16 17 75 84 85 86 96 88 99 102	funcco	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ( ⟨ ⟨ 𝑋 , 𝑧 ⟩ , ⟨ 𝑌 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑌 , 𝑤 ⟩ ) ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) ) = ( ( ( ⟨ 𝑌 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) ) )
104	83 95 103	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( ⟨ 𝑋 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) ) = ( ( ( ⟨ 𝑌 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) ) )
105	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
106	1 2 58 66 105 6 59 41 67	curf11	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑧 ) )
107	106 43	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) )
108	1 2 58 66 105 6 59 41 69	curf11	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑤 ) )
109		df-ov	⊢ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ )
110	108 109	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) )
111	107 110	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ⟩ )
112	1 2 58 66 105 6 61 45 69	curf11	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) = ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑤 ) )
113		df-ov	⊢ ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ )
114	112 113	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) )
115	111 114	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) )
116	1 2 58 66 105 6 7 8 59 61 62 12 69	curf2val	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐿 ‘ 𝑤 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ( 𝐼 ‘ 𝑤 ) ) )
117		df-ov	⊢ ( 𝐾 ( ⟨ 𝑋 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ( 𝐼 ‘ 𝑤 ) ) = ( ( ⟨ 𝑋 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ )
118	116 117	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐿 ‘ 𝑤 ) = ( ( ⟨ 𝑋 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ) )
119	1 2 58 66 105 6 59 41 67 28 57 69 70	curf12	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑤 ) ‘ 𝑓 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) 𝑓 ) )
120		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) 𝑓 ) = ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ )
121	119 120	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑤 ) ‘ 𝑓 ) = ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) )
122	115 118 121	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝐿 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑤 ) ‘ 𝑓 ) ) = ( ( ( ⟨ 𝑋 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑓 ⟩ ) ) )
123	1 2 58 66 105 6 61 45 67	curf11	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) = ( 𝑌 ( 1^st ‘ 𝐹 ) 𝑧 ) )
124	123 47	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) )
125	107 124	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ⟩ )
126	125 114	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) )
127	1 2 58 66 105 6 61 45 67 28 57 69 70	curf12	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) 𝑤 ) ‘ 𝑓 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑌 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) 𝑓 ) )
128		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑌 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) 𝑓 ) = ( ( ⟨ 𝑌 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ )
129	127 128	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) 𝑤 ) ‘ 𝑓 ) = ( ( ⟨ 𝑌 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ) )
130	1 2 58 66 105 6 7 8 59 61 62 12 67	curf2val	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐿 ‘ 𝑧 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) )
131		df-ov	⊢ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) = ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ )
132	130 131	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝐿 ‘ 𝑧 ) = ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) )
133	126 129 132	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) 𝑤 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( 𝐿 ‘ 𝑧 ) ) = ( ( ( ⟨ 𝑌 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , 𝑓 ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑌 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ‘ ⟨ 𝐾 , ( 𝐼 ‘ 𝑧 ) ⟩ ) ) )
134	104 122 133	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝐿 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑤 ) ‘ 𝑓 ) ) = ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) 𝑤 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( 𝐿 ‘ 𝑧 ) ) )
135	134	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ( ( 𝐿 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑤 ) ‘ 𝑓 ) ) = ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) 𝑤 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( 𝐿 ‘ 𝑧 ) ) )
136	1 2 3 4 5 6 9 41	curf1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐸 ) )
137	1 2 3 4 5 6 10 45	curf1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ∈ ( 𝐷 Func 𝐸 ) )
138	13 6 28 18 84 136 137	isnat2	⊢ ( 𝜑 → ( 𝐿 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ↔ ( 𝐿 ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ( ( 𝐿 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑤 ) ‘ 𝑓 ) ) = ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) 𝑤 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ‘ 𝑤 ) ) ( 𝐿 ‘ 𝑧 ) ) ) ) )
139	56 135 138	mpbir2and	⊢ ( 𝜑 → 𝐿 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem curf2cl

Proof