Theorem prfcl 18220

Description: The pairing of functors 𝐹:𝐶⟶𝐷 and 𝐺:𝐶⟶𝐷 is a functor ⟨𝐹, 𝐺⟩:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.)

Hypotheses

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

Assertion

Ref	Expression
prfcl	⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇))

Proof of Theorem prfcl

Dummy variables 𝑓 𝑔 ℎ 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  Vcvv 3464  ⟨cop 4612   class class class wbr 5124   ↦ cmpt 5206   × cxp 5657  Rel wrel 5664   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410   ∈ cmpo 7412  1^st c1st 7991  2^nd c2nd 7992  Basecbs 17233  Hom chom 17287  compcco 17288  Catccat 17681  Idccid 17682   Func cfunc 17872   ×_c cxpc 18185   ⟨,⟩_F cprf 18188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8724  df-map 8847  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12507  df-z 12594  df-dec 12714  df-uz 12858  df-fz 13530  df-struct 17171  df-slot 17206  df-ndx 17218  df-base 17234  df-hom 17300  df-cco 17301  df-cat 17685  df-cid 17686  df-func 17876  df-xpc 18189  df-prf 18192

This theorem is referenced by:  prf1st  18221  prf2nd  18222  uncfcl  18252  uncf1  18253  uncf2  18254  yonedalem1  18289  yonedalem21  18290  yonedalem22  18295