curf1cl

Description: The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
	curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
	curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	curf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	curf1.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 )
Assertion	curf1cl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
2		curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
6		curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		curf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		curf1.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 )
9		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11	1 2 3 4 5 6 7 8 9 10	curf1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
12	6	fvexi	⊢ 𝐵 ∈ V
13	12	mptex	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) ∈ V
14	12 12	mpoex	⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ∈ V
15	13 14	op1std	⊢ ( 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
16	11 15	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
17	13 14	op2ndd	⊢ ( 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ → ( 2^nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
18	11 17	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
19	16 18	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
20	11 19	eqtr4d	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
21		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
22		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
23		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
24		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
25		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
26		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
27		funcrcl	⊢ ( 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) → ( ( 𝐶 ×_c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
28	5 27	syl	⊢ ( 𝜑 → ( ( 𝐶 ×_c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
29	28	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
30		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
31	30 2 6	xpcbas	⊢ ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
32		relfunc	⊢ Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 )
33		1st2ndbr	⊢ ( ( Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ∧ 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
34	32 5 33	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
35	31 21 34	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( 𝐴 × 𝐵 ) ⟶ ( Base ‘ 𝐸 ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1^st ‘ 𝐹 ) : ( 𝐴 × 𝐵 ) ⟶ ( Base ‘ 𝐸 ) )
37	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
38		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
39	36 37 38	fovrnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
40	16 39	fmpt3d	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : 𝐵 ⟶ ( Base ‘ 𝐸 ) )
41		eqid	⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) )
42		ovex	⊢ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∈ V
43	42	mptex	⊢ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V
44	41 43	fnmpoi	⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) Fn ( 𝐵 × 𝐵 )
45	18	fneq1d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝐾 ) Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) Fn ( 𝐵 × 𝐵 ) ) )
46	44 45	mpbiri	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) Fn ( 𝐵 × 𝐵 ) )
47	18	oveqd	⊢ ( 𝜑 → ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) = ( 𝑦 ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) 𝑧 ) )
48	41	ovmpt4g	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V ) → ( 𝑦 ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) 𝑧 ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) )
49	43 48	mp3an3	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) 𝑧 ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) )
50	47 49	sylan9eq	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) )
51		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
52	34	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
53	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑋 ∈ 𝐴 )
54		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑦 ∈ 𝐵 )
55	53 54	opelxpd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ 𝑋 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
56		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑧 ∈ 𝐵 )
57	53 56	opelxpd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ 𝑋 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
58	31 51 22 52 55 57	funcf2	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) : ( ⟨ 𝑋 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑧 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) )
59		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
60	30 31 59 9 51 55 57	xpchom	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ⟨ 𝑋 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑧 ⟩ ) = ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) × ( ( 2^nd ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) ) )
61	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐶 ∈ Cat )
62	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐷 ∈ Cat )
63	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
64	1 2 61 62 63 6 53 8 54	curf11	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) )
65		df-ov	⊢ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ )
66	64 65	eqtr2di	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) = ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) )
67	1 2 61 62 63 6 53 8 56	curf11	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑧 ) )
68		df-ov	⊢ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ )
69	67 68	eqtr2di	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) = ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) )
70	66 69	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) = ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ) )
71	60 70	feq23d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) : ( ⟨ 𝑋 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑧 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) ↔ ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) : ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) × ( ( 2^nd ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) ) ⟶ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ) ) )
72	58 71	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) : ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) × ( ( 2^nd ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) ) ⟶ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ) )
73	2 59 10 61 53	catidcl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
74		op1stg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑦 ⟩ ) = 𝑋 )
75	53 54 74	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( 1^st ‘ ⟨ 𝑋 , 𝑦 ⟩ ) = 𝑋 )
76		op1stg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑧 ⟩ ) = 𝑋 )
77	53 56 76	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( 1^st ‘ ⟨ 𝑋 , 𝑧 ⟩ ) = 𝑋 )
78	75 77	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
79	73 78	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( ( 1^st ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) )
80		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
81		op2ndg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑦 ⟩ ) = 𝑦 )
82	53 54 81	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑦 ⟩ ) = 𝑦 )
83		op2ndg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑧 ⟩ ) = 𝑧 )
84	53 56 83	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑧 ⟩ ) = 𝑧 )
85	82 84	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 2^nd ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) = ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
86	80 85	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑔 ∈ ( ( 2^nd ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ) )
87	72 79 86	fovrnd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ) )
88	50 87	fmpt3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ) )
89	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Cat )
90	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ Cat )
91		eqid	⊢ ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Id ‘ ( 𝐶 ×_c 𝐷 ) )
92	30 89 90 2 6 10 23 91 37 38	xpcid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ )
93	92	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ) = ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ ) )
94		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ )
95	93 94	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) )
96	34	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
97		opelxpi	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
98	7 97	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
99	31 91 24 96 98	funcid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ) )
100	95 99	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ) )
101	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
102	6 9 23 90 38	catidcl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑦 ) )
103	1 2 89 90 101 6 37 8 38 9 10 38 102	curf12	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑦 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) )
104	1 2 89 90 101 6 37 8 38	curf11	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) )
105	104 65	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) )
106	105	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) ) )
107	100 103 106	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑦 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ) )
108	7	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑋 ∈ 𝐴 )
109		simp21	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑦 ∈ 𝐵 )
110		simp22	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑧 ∈ 𝐵 )
111		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
112		eqid	⊢ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) = ( comp ‘ ( 𝐶 ×_c 𝐷 ) )
113		simp23	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑤 ∈ 𝐵 )
114	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
115	2 59 10 114 108	catidcl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
116		simp3l	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
117		simp3r	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) )
118	30 2 6 59 9 108 109 108 110 111 25 112 108 113 115 116 115 117	xpcco2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ( ⟨ ⟨ 𝑋 , 𝑦 ⟩ , ⟨ 𝑋 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) = ⟨ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) , ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
119	2 59 10 114 108 111 108 115	catlid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
120	119	opeq1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) , ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ = ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
121	118 120	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ( ⟨ ⟨ 𝑋 , 𝑦 ⟩ , ⟨ 𝑋 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
122	121	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ( ⟨ ⟨ 𝑋 , 𝑦 ⟩ , ⟨ 𝑋 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) ) = ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ ) )
123		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
124	122 123	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ( ⟨ ⟨ 𝑋 , 𝑦 ⟩ , ⟨ 𝑋 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) )
125	34	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
126	108 109	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑋 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
127	108 110	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑋 , 𝑧 ⟩ ∈ ( 𝐴 × 𝐵 ) )
128	108 113	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑋 , 𝑤 ⟩ ∈ ( 𝐴 × 𝐵 ) )
129	115 116	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ∈ ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
130	30 2 6 59 9 108 109 108 110 51	xpchom2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑋 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑧 ⟩ ) = ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
131	129 130	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ∈ ( ⟨ 𝑋 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑧 ⟩ ) )
132	115 117	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ∈ ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
133	30 2 6 59 9 108 110 108 113 51	xpchom2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) = ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
134	132 133	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ∈ ( ⟨ 𝑋 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) )
135	31 51 112 26 125 126 127 128 131 134	funcco	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ( ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ( ⟨ ⟨ 𝑋 , 𝑦 ⟩ , ⟨ 𝑋 , 𝑧 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑋 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) ) = ( ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) ) )
136	124 135	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) ) )
137	4	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐷 ∈ Cat )
138	5	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
139	6 9 25 137 109 110 113 116 117	catcocl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) )
140	1 2 114 137 138 6 108 8 109 9 10 113 139	curf12	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑤 ) ‘ ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) )
141	1 2 114 137 138 6 108 8 109	curf11	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) )
142	141 65	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) )
143	1 2 114 137 138 6 108 8 110	curf11	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑧 ) )
144	143 68	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) )
145	142 144	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ⟩ )
146	1 2 114 137 138 6 108 8 113	curf11	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑤 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑤 ) )
147		df-ov	⊢ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ )
148	146 147	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) )
149	145 148	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ) )
150	1 2 114 137 138 6 108 8 110 9 10 113 117	curf12	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐾 ) 𝑤 ) ‘ ℎ ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ℎ ) )
151		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ℎ ) = ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ )
152	150 151	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐾 ) 𝑤 ) ‘ ℎ ) = ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ) )
153	1 2 114 137 138 6 108 8 109 9 10 110 116	curf12	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑔 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) )
154		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) = ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ )
155	153 154	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑔 ) = ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) )
156	149 152 155	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐾 ) 𝑤 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑔 ) ) = ( ( ( ⟨ 𝑋 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ℎ ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑧 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , 𝑔 ⟩ ) ) )
157	136 140 156	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑤 ) ‘ ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐾 ) 𝑤 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑔 ) ) )
158	6 21 9 22 23 24 25 26 4 29 40 46 88 107 157	isfuncd	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
159		df-br	⊢ ( ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) ↔ ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∈ ( 𝐷 Func 𝐸 ) )
160	158 159	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∈ ( 𝐷 Func 𝐸 ) )
161	20 160	eqeltrd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )

Metamath Proof Explorer

Theorem curf1cl

Proof