Theorem prfcl 18109

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 2731	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		eqid 2731	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
4		prfcl.c	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
5		prfcl.d	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))
6	1, 2, 3, 4, 5	prfval 18105	. . 3 ⊢ (𝜑 → 𝑃 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
7		fvex 6835	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
8	7	mptex 7157	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩) ∈ V
9	7, 7	mpoex 8011	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)) ∈ V
10	8, 9	op1std 7931	. . . . 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 7932	. . . . 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 4830	. . 3 ⊢ (𝜑 → ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩ = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
15	6, 14	eqtr4d 2769	. 2 ⊢ (𝜑 → 𝑃 = ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩)
16		prfcl.t	. . . . 5 ⊢ 𝑇 = (𝐷 ×c 𝐸)
17		eqid 2731	. . . . 5 ⊢ (Base‘𝐷) = (Base‘𝐷)
18		eqid 2731	. . . . 5 ⊢ (Base‘𝐸) = (Base‘𝐸)
19	16, 17, 18	xpcbas 18084	. . . 4 ⊢ ((Base‘𝐷) × (Base‘𝐸)) = (Base‘𝑇)
20		eqid 2731	. . . 4 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
21		eqid 2731	. . . 4 ⊢ (Id‘𝐶) = (Id‘𝐶)
22		eqid 2731	. . . 4 ⊢ (Id‘𝑇) = (Id‘𝑇)
23		eqid 2731	. . . 4 ⊢ (comp‘𝐶) = (comp‘𝐶)
24		eqid 2731	. . . 4 ⊢ (comp‘𝑇) = (comp‘𝑇)
25		funcrcl 17770	. . . . . 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 17770	. . . . . . 7 ⊢ (𝐺 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
30	5, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
31	30	simprd 495	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Cat)
32	16, 28, 31	xpccat 18096	. . . 4 ⊢ (𝜑 → 𝑇 ∈ Cat)
33		relfunc 17769	. . . . . . . . 9 ⊢ Rel (𝐶 Func 𝐷)
34		1st2ndbr 7974	. . . . . . . . 9 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
35	33, 4, 34	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
36	2, 17, 35	funcf1 17773	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
37	36	ffvelcdmda 7017	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
38		relfunc 17769	. . . . . . . . 9 ⊢ Rel (𝐶 Func 𝐸)
39		1st2ndbr 7974	. . . . . . . . 9 ⊢ ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
40	38, 5, 39	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
41	2, 18, 40	funcf1 17773	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐸))
42	41	ffvelcdmda 7017	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸))
43	37, 42	opelxpd 5653	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ ∈ ((Base‘𝐷) × (Base‘𝐸)))
44	11, 43	fmpt3d 7049	. . . 4 ⊢ (𝜑 → (1st ‘𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)))
45		eqid 2731	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))
46		ovex 7379	. . . . . . 7 ⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V
47	46	mptex 7157	. . . . . 6 ⊢ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩) ∈ V
48	45, 47	fnmpoi 8002	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)) Fn ((Base‘𝐶) × (Base‘𝐶))
49	13	fneq1d 6574	. . . . 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 7363	. . . . . 6 ⊢ (𝜑 → (𝑥(2nd ‘𝑃)𝑦) = (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))𝑦))
52	45	ovmpt4g 7493	. . . . . . 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 2786	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))
55		eqid 2731	. . . . . . . . 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 17775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
60	59	ffvelcdmda 7017	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐹)𝑦)‘ℎ) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
61		eqid 2731	. . . . . . . . 9 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
62	40	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
63	2, 3, 61, 62, 57, 58	funcf2 17775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
64	63	ffvelcdmda 7017	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘ℎ) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
65	60, 64	opelxpd 5653	. . . . . 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 18106	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑥) = ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩)
69	1, 2, 3, 66, 67, 58	prf1 18106	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑦) = ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩)
70	68, 69	oveq12d 7364	. . . . . . . 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 7017	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
74	73	adantrl 716	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
75	41	ffvelcdmda 7017	. . . . . . . . . 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 18092	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩(Hom ‘𝑇)⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))))
78	70, 77	eqtrd 2766	. . . . . . 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 2834	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩ ∈ (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)))
81	54, 80	fmpt3d 7049	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)))
82		eqid 2731	. . . . . . 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 17777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)))
86		eqid 2731	. . . . . . 7 ⊢ (Id‘𝐸) = (Id‘𝐸)
87	40	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
88	2, 21, 86, 87, 84	funcid 17777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥)))
89	85, 88	opeq12d 4830	. . . . 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 17588	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
94	1, 2, 3, 90, 91, 84, 84, 93	prf2 18108	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ⟨((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))⟩)
95	1, 2, 3, 90, 91, 84	prf1 18106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝑃)‘𝑥) = ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩)
96	95	fveq2d 6826	. . . . . 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 18095	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩) = ⟨((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))⟩)
100	96, 99	eqtrd 2766	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)) = ⟨((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))⟩)
101	89, 94, 100	3eqtr4d 2776	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)))
102		eqid 2731	. . . . . . 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 17778	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
110		eqid 2731	. . . . . . 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 17778	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(⟨((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)⟩(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓)))
114	109, 113	opeq12d 4830	. . . . 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 17591	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
118	1, 2, 3, 115, 111, 104, 106, 117	prf2 18108	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ⟨((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))⟩)
119	1, 2, 3, 115, 111, 104	prf1 18106	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑥) = ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩)
120	1, 2, 3, 115, 111, 105	prf1 18106	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑦) = ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩)
121	119, 120	opeq12d 4830	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)⟩ = ⟨⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩, ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩⟩)
122	1, 2, 3, 115, 111, 106	prf1 18106	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑧) = ⟨((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)⟩)
123	121, 122	oveq12d 7364	. . . . . . 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 18108	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝑃)𝑧)‘𝑔) = ⟨((𝑦(2nd ‘𝐹)𝑧)‘𝑔), ((𝑦(2nd ‘𝐺)𝑧)‘𝑔)⟩)
125	1, 2, 3, 115, 111, 104, 105, 107	prf2 18108	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) = ⟨((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)⟩)
126	123, 124, 125	oveq123d 7367	. . . . . 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 7018	. . . . . . 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 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸))
131	127, 105	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
132	129, 105	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸))
133	127, 106	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷))
134	129, 106	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑧) ∈ (Base‘𝐸))
135	2, 3, 55, 103, 104, 105	funcf2 17775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
136	135, 107	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
137	2, 3, 61, 112, 104, 105	funcf2 17775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
138	137, 107	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
139	2, 3, 55, 103, 105, 106	funcf2 17775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
140	139, 108	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
141	2, 3, 61, 112, 105, 106	funcf2 17775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐺)‘𝑦)(Hom ‘𝐸)((1st ‘𝐺)‘𝑧)))
142	141, 108	ffvelcdmd 7018	. . . . . . 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 18093	. . . . . 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 2766	. . . . 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 2776	. . . 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 17772	. . 3 ⊢ (𝜑 → (1st ‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃))
147		df-br 5090	. . 3 ⊢ ((1st ‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃) ↔ ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩ ∈ (𝐶 Func 𝑇))
148	146, 147	sylib 218	. 2 ⊢ (𝜑 → ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩ ∈ (𝐶 Func 𝑇))
149	15, 148	eqeltrd 2831	1 ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ⟨cop 4579   class class class wbr 5089   ↦ cmpt 5170   × cxp 5612  Rel wrel 5619   Fn wfn 6476  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346   ∈ cmpo 7348  1^st c1st 7919  2^nd c2nd 7920  Basecbs 17120  Hom chom 17172  compcco 17173  Catccat 17570  Idccid 17571   Func cfunc 17761   ×_c cxpc 18074   ⟨,⟩_F cprf 18077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-er 8622  df-map 8752  df-ixp 8822  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-nn 12126  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192  df-7 12193  df-8 12194  df-9 12195  df-n0 12382  df-z 12469  df-dec 12589  df-uz 12733  df-fz 13408  df-struct 17058  df-slot 17093  df-ndx 17105  df-base 17121  df-hom 17185  df-cco 17186  df-cat 17574  df-cid 17575  df-func 17765  df-xpc 18078  df-prf 18081

This theorem is referenced by:  prf1st  18110  prf2nd  18111  uncfcl  18141  uncf1  18142  uncf2  18143  yonedalem1  18178  yonedalem21  18179  yonedalem22  18184