Theorem 1stfcl

Description: The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	1stfcl.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	1stfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	1stfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	1stfcl.p	⊢ 𝑃 = ( 𝐶 1stF 𝐷 )
Assertion	1stfcl	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑇 Func 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		1stfcl.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		1stfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		1stfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		1stfcl.p	⊢ 𝑃 = ( 𝐶 1stF 𝐷 )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7	1 5 6	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑇 )
8		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
9	1 7 8 2 3 4	1stfval	⊢ ( 𝜑 → 𝑃 = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ )
10		fo1st	⊢ 1st : V –onto→ V
11		fofun	⊢ ( 1st : V –onto→ V → Fun 1st )
12	10 11	ax-mp	⊢ Fun 1st
13		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
14		fvex	⊢ ( Base ‘ 𝐷 ) ∈ V
15	13 14	xpex	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∈ V
16		resfunexg	⊢ ( ( Fun 1st ∧ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∈ V ) → ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∈ V )
17	12 15 16	mp2an	⊢ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∈ V
18	15 15	mpoex	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ∈ V
19	17 18	op2ndd	⊢ ( 𝑃 = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) )
20	9 19	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) )
21	20	opeq2d	⊢ ( 𝜑 → ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ )
22	9 21	eqtr4d	⊢ ( 𝜑 → 𝑃 = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ )
23		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
24		eqid	⊢ ( Id ‘ 𝑇 ) = ( Id ‘ 𝑇 )
25		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
26		eqid	⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
27		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
28	1 2 3	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
29		f1stres	⊢ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐶 )
30	29	a1i	⊢ ( 𝜑 → ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐶 ) )
31		eqid	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
32		ovex	⊢ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∈ V
33		resfunexg	⊢ ( ( Fun 1st ∧ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∈ V ) → ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ∈ V )
34	12 32 33	mp2an	⊢ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ∈ V
35	31 34	fnmpoi	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
36	20	fneq1d	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑃 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ↔ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) )
37	35 36	mpbiri	⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) )
38		f1stres	⊢ ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) )
39	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝐶 ∈ Cat )
40	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝐷 ∈ Cat )
41		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
42		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
43	1 7 8 39 40 4 41 42	1stf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
44		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
45	1 7 23 44 8 41 42	xpchom	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) = ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) )
46	45	reseq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) = ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) )
47	43 46	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) )
48	47	feq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) ↔ ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) ) )
49	38 48	mpbiri	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) )
50		fvres	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
51	50	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
52		fvres	⊢ ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 1st ‘ 𝑦 ) )
53	52	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 1st ‘ 𝑦 ) )
54	51 53	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) = ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) )
55	45 54	feq23d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ⟶ ( ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) ↔ ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) ) )
56	49 55	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ⟶ ( ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) )
57	28	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑇 ∈ Cat )
58		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
59	7 8 24 57 58	catidcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) )
60	59	fvresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( 1st ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) )
61		1st2nd2	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
62	61	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
63	62	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) = ( ( Id ‘ 𝑇 ) ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
64	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝐶 ∈ Cat )
65	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝐷 ∈ Cat )
66		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
67		xp1st	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 1st ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 1st ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
69		xp2nd	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 2nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
70	69	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 2nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
71	1 64 65 5 6 25 66 24 68 70	xpcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) , ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ )
72	63 71	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) , ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ )
73		fvex	⊢ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) ∈ V
74		fvex	⊢ ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ∈ V
75	73 74	op1std	⊢ ( ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) , ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ → ( 1st ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
76	72 75	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 1st ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
77	60 76	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
78	1 7 8 64 65 4 58 58	1stf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) )
79	78	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) )
80	50	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
81	80	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
82	77 79 81	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) )
83	28	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑇 ∈ Cat )
84		simp21	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
85		simp22	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
86		simp23	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
87		simp3l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) )
88		simp3r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) )
89	7 8 26 83 84 85 86 87 88	catcocl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) )
90	89	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( 1st ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) )
91	1 7 8 26 84 85 86 87 88 27	xpcco1st	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 1st ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 1st ‘ 𝑔 ) ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) ( 1st ‘ 𝑓 ) ) )
92	90 91	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 1st ‘ 𝑔 ) ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) ( 1st ‘ 𝑓 ) ) )
93	2	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
94	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝐷 ∈ Cat )
95	1 7 8 93 94 4 84 86	1stf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) )
96	95	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) )
97	84	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
98	85	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 1st ‘ 𝑦 ) )
99	97 98	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ = ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ )
100	86	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) = ( 1st ‘ 𝑧 ) )
101	99 100	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) = ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) )
102	1 7 8 93 94 4 85 86	1stf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) = ( 1st ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) )
103	102	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) = ( ( 1st ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ 𝑔 ) )
104	88	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ 𝑔 ) = ( 1st ‘ 𝑔 ) )
105	103 104	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) = ( 1st ‘ 𝑔 ) )
106	1 7 8 93 94 4 84 85	1stf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
107	106	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) = ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ‘ 𝑓 ) )
108	87	fvresd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ‘ 𝑓 ) = ( 1st ‘ 𝑓 ) )
109	107 108	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) = ( 1st ‘ 𝑓 ) )
110	101 105 109	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 1st ‘ 𝑔 ) ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) ( 1st ‘ 𝑓 ) ) )
111	92 96 110	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
112	7 5 8 23 24 25 26 27 28 2 30 37 56 82 111	isfuncd	⊢ ( 𝜑 → ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ( 𝑇 Func 𝐶 ) ( 2nd ‘ 𝑃 ) )
113		df-br	⊢ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ( 𝑇 Func 𝐶 ) ( 2nd ‘ 𝑃 ) ↔ ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( 𝑇 Func 𝐶 ) )
114	112 113	sylib	⊢ ( 𝜑 → ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( 𝑇 Func 𝐶 ) )
115	22 114	eqeltrd	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑇 Func 𝐶 ) )