prfcl

Description: The pairing of functors F : C --> D and G : C --> D is a functor <. F , G >. : C --> ( D X. E ) . (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	prfcl.p	⊢ 𝑃 = ( 𝐹 ⟨,⟩_F 𝐺 )
	prfcl.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐸 )
	prfcl.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	prfcl.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
Assertion	prfcl	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐶 Func 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		prfcl.p	⊢ 𝑃 = ( 𝐹 ⟨,⟩_F 𝐺 )
2		prfcl.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐸 )
3		prfcl.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4		prfcl.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7	1 5 6 3 4	prfval	⊢ ( 𝜑 → 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
8		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
9	8	mptex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) ∈ V
10	8 8	mpoex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ∈ V
11	9 10	op1std	⊢ ( 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ → ( 1^st ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
12	7 11	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
13	9 10	op2ndd	⊢ ( 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ → ( 2^nd ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) )
14	7 13	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) )
15	12 14	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
16	7 15	eqtr4d	⊢ ( 𝜑 → 𝑃 = ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ )
17		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
19	2 17 18	xpcbas	⊢ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) = ( Base ‘ 𝑇 )
20		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
21		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
22		eqid	⊢ ( Id ‘ 𝑇 ) = ( Id ‘ 𝑇 )
23		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
24		eqid	⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
25		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
26	3 25	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
27	26	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
28	26	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
29		funcrcl	⊢ ( 𝐺 ∈ ( 𝐶 Func 𝐸 ) → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
30	4 29	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
31	30	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
32	2 28 31	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
33		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
34		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
35	33 3 34	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
36	5 17 35	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
37	36	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
38		relfunc	⊢ Rel ( 𝐶 Func 𝐸 )
39		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
40	38 4 39	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
41	5 18 40	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
42	41	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
43	37 42	opelxpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
44	12 43	fmpt3d	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) : ( Base ‘ 𝐶 ) ⟶ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
45		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
46		ovex	⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
47	46	mptex	⊢ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ∈ V
48	45 47	fnmpoi	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
49	14	fneq1d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑃 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
50	48 49	mpbiri	⊢ ( 𝜑 → ( 2^nd ‘ 𝑃 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
51	14	oveqd	⊢ ( 𝜑 → ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) 𝑦 ) )
52	45	ovmpt4g	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ∈ V ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) 𝑦 ) = ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
53	47 52	mp3an3	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) 𝑦 ) = ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
54	51 53	sylan9eq	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) = ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
55		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
56	35	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
57		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
58		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
59	5 6 55 56 57 58	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
60	59	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
61		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
62	40	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
63	5 6 61 62 57 58	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
64	63	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
65	60 64	opelxpd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ∈ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
66	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
67	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
68	1 5 6 66 67 57	prf1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
69	1 5 6 66 67 58	prf1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ )
70	68 69	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( Hom ‘ 𝑇 ) ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ) )
71	37	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
72	42	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
73	36	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
74	73	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
75	41	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
76	75	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
77	2 17 18 55 61 71 72 74 76 20	xpchom2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( Hom ‘ 𝑇 ) ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
78	70 77	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
79	78	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
80	65 79	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ∈ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) )
81	54 80	fmpt3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) )
82		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
83	35	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
84		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
85	5 21 82 83 84	funcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
86		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
87	40	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
88	5 21 86 87 84	funcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
89	85 88	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ⟩ = ⟨ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
90	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
91	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
92	27	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
93	5 6 21 92 84	catidcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
94	1 5 6 90 91 84 84 93	prf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ⟩ )
95	1 5 6 90 91 84	prf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
96	95	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑇 ) ‘ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑇 ) ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
97	28	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
98	31	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
99	2 97 98 17 18 82 86 22 37 42	xpcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑇 ) ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) = ⟨ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
100	96 99	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑇 ) ‘ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ) = ⟨ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
101	89 94 100	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑇 ) ‘ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ) )
102		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
103	35	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
104		simp21	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
105		simp22	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
106		simp23	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
107		simp3l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
108		simp3r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
109	5 6 23 102 103 104 105 106 107 108	funcco	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
110		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
111	4	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
112	38 111 39	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
113	5 6 23 110 112 104 105 106 107 108	funcco	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) )
114	109 113	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ⟩ = ⟨ ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
115	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
116	27	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
117	5 6 23 116 104 105 106 107 108	catcocl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
118	1 5 6 115 111 104 106 117	prf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ⟩ )
119	1 5 6 115 111 104	prf1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
120	1 5 6 115 111 105	prf1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ )
121	119 120	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ⟨ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ = ⟨ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ )
122	1 5 6 115 111 106	prf1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑧 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ )
123	121 122	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ⟨ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑧 ) ) = ( ⟨ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ 𝑇 ) ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ) )
124	1 5 6 115 111 105 106 108	prf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) = ⟨ ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) , ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ⟩ )
125	1 5 6 115 111 104 105 107	prf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) = ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ )
126	123 124 125	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ⟨ ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) , ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ⟩ ( ⟨ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ 𝑇 ) ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ) ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) )
127	36	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
128	127 104	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
129	41	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
130	129 104	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
131	127 105	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
132	129 105	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
133	127 106	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
134	129 106	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐸 ) )
135	5 6 55 103 104 105	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
136	135 107	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
137	5 6 61 112 104 105	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
138	137 107	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
139	5 6 55 103 105 106	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
140	139 108	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
141	5 6 61 112 105 106	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
142	141 108	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
143	2 17 18 55 61 128 130 131 132 102 110 24 133 134 136 138 140 142	xpcco2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ⟨ ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) , ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ⟩ ( ⟨ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ 𝑇 ) ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ) ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) = ⟨ ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
144	126 143	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ⟨ ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
145	114 118 144	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
146	5 19 6 20 21 22 23 24 27 32 44 50 81 101 145	isfuncd	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) ( 𝐶 Func 𝑇 ) ( 2^nd ‘ 𝑃 ) )
147		df-br	⊢ ( ( 1^st ‘ 𝑃 ) ( 𝐶 Func 𝑇 ) ( 2^nd ‘ 𝑃 ) ↔ ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ ∈ ( 𝐶 Func 𝑇 ) )
148	146 147	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑃 ) , ( 2^nd ‘ 𝑃 ) ⟩ ∈ ( 𝐶 Func 𝑇 ) )
149	16 148	eqeltrd	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐶 Func 𝑇 ) )

Metamath Proof Explorer

Theorem prfcl

Proof