Theorem prfcl 16666

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 2610	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		eqid 2610	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
4		prfcl.c	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
5		prfcl.d	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸))
6	1, 2, 3, 4, 5	prfval 16662	. . 3 ⊢ (𝜑 → 𝑃 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
7		fvex 6113	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
8	7	mptex 6390	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩) ∈ V
9	7, 7	mpt2ex 7136	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)) ∈ V
10	8, 9	op1std 7069	. . . . 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 7070	. . . . 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 4348	. . 3 ⊢ (𝜑 → ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩ = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))⟩)
15	6, 14	eqtr4d 2647	. 2 ⊢ (𝜑 → 𝑃 = ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩)
16		prfcl.t	. . . . 5 ⊢ 𝑇 = (𝐷 ×c 𝐸)
17		eqid 2610	. . . . 5 ⊢ (Base‘𝐷) = (Base‘𝐷)
18		eqid 2610	. . . . 5 ⊢ (Base‘𝐸) = (Base‘𝐸)
19	16, 17, 18	xpcbas 16641	. . . 4 ⊢ ((Base‘𝐷) × (Base‘𝐸)) = (Base‘𝑇)
20		eqid 2610	. . . 4 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
21		eqid 2610	. . . 4 ⊢ (Id‘𝐶) = (Id‘𝐶)
22		eqid 2610	. . . 4 ⊢ (Id‘𝑇) = (Id‘𝑇)
23		eqid 2610	. . . 4 ⊢ (comp‘𝐶) = (comp‘𝐶)
24		eqid 2610	. . . 4 ⊢ (comp‘𝑇) = (comp‘𝑇)
25		funcrcl 16346	. . . . . 6 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
26	4, 25	syl 17	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
27	26	simpld 474	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
28	26	simprd 478	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ Cat)
29		funcrcl 16346	. . . . . . 7 ⊢ (𝐺 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
30	5, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
31	30	simprd 478	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Cat)
32	16, 28, 31	xpccat 16653	. . . 4 ⊢ (𝜑 → 𝑇 ∈ Cat)
33		relfunc 16345	. . . . . . . . . 10 ⊢ Rel (𝐶 Func 𝐷)
34		1st2ndbr 7108	. . . . . . . . . 10 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
35	33, 4, 34	sylancr 694	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
36	2, 17, 35	funcf1 16349	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
37	36	ffvelrnda 6267	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
38		relfunc 16345	. . . . . . . . . 10 ⊢ Rel (𝐶 Func 𝐸)
39		1st2ndbr 7108	. . . . . . . . . 10 ⊢ ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
40	38, 5, 39	sylancr 694	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
41	2, 18, 40	funcf1 16349	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐸))
42	41	ffvelrnda 6267	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸))
43		opelxpi 5072	. . . . . . 7 ⊢ ((((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷) ∧ ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) → ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ ∈ ((Base‘𝐷) × (Base‘𝐸)))
44	37, 42, 43	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩ ∈ ((Base‘𝐷) × (Base‘𝐸)))
45		eqid 2610	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩) = (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩)
46	44, 45	fmptd 6292	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)))
47	11	feq1d 5943	. . . . 5 ⊢ (𝜑 → ((1st ‘𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)) ↔ (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸))))
48	46, 47	mpbird 246	. . . 4 ⊢ (𝜑 → (1st ‘𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)))
49		eqid 2610	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))
50		ovex 6577	. . . . . . 7 ⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V
51	50	mptex 6390	. . . . . 6 ⊢ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩) ∈ V
52	49, 51	fnmpt2i 7128	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)) Fn ((Base‘𝐶) × (Base‘𝐶))
53	13	fneq1d 5895	. . . . 5 ⊢ (𝜑 → ((2nd ‘𝑃) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)) Fn ((Base‘𝐶) × (Base‘𝐶))))
54	52, 53	mpbiri 247	. . . 4 ⊢ (𝜑 → (2nd ‘𝑃) Fn ((Base‘𝐶) × (Base‘𝐶)))
55		eqid 2610	. . . . . . . . . 10 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
56	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
57		simprl 790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
58		simprr 792	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
59	2, 3, 55, 56, 57, 58	funcf2 16351	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
60	59	ffvelrnda 6267	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐹)𝑦)‘ℎ) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
61		eqid 2610	. . . . . . . . . 10 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
62	40	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
63	2, 3, 61, 62, 57, 58	funcf2 16351	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
64	63	ffvelrnda 6267	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘ℎ) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
65		opelxpi 5072	. . . . . . . 8 ⊢ ((((𝑥(2nd ‘𝐹)𝑦)‘ℎ) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ ((𝑥(2nd ‘𝐺)𝑦)‘ℎ) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) → ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩ ∈ ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))))
66	60, 64, 65	syl2anc 691	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩ ∈ ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))))
67	4	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
68	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐶 Func 𝐸))
69	1, 2, 3, 67, 68, 57	prf1 16663	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑥) = ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩)
70	1, 2, 3, 67, 68, 58	prf1 16663	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑦) = ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩)
71	69, 70	oveq12d 6567	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) = (⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩(Hom ‘𝑇)⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩))
72	37	adantrr 749	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
73	42	adantrr 749	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸))
74	36	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
75	74	adantrl 748	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
76	41	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸))
77	76	adantrl 748	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸))
78	16, 17, 18, 55, 61, 72, 73, 75, 77, 20	xpchom2 16649	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩(Hom ‘𝑇)⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))))
79	71, 78	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))))
80	79	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))))
81	66, 80	eleqtrrd 2691	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩ ∈ (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)))
82		eqid 2610	. . . . . 6 ⊢ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩)
83	81, 82	fmptd 6292	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)))
84	13	oveqd 6566	. . . . . . 7 ⊢ (𝜑 → (𝑥(2nd ‘𝑃)𝑦) = (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))𝑦))
85	49	ovmpt4g 6681	. . . . . . . 8 ⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩) ∈ V) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))
86	51, 85	mp3an3 1405	. . . . . . 7 ⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))
87	84, 86	sylan9eq 2664	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩))
88	87	feq1d 5943	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) ↔ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)⟩):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦))))
89	83, 88	mpbird 246	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)))
90		eqid 2610	. . . . . . 7 ⊢ (Id‘𝐷) = (Id‘𝐷)
91	35	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
92		simpr 476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
93	2, 21, 90, 91, 92	funcid 16353	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)))
94		eqid 2610	. . . . . . 7 ⊢ (Id‘𝐸) = (Id‘𝐸)
95	40	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
96	2, 21, 94, 95, 92	funcid 16353	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥)))
97	93, 96	opeq12d 4348	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ⟨((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))⟩ = ⟨((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))⟩)
98	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
99	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐶 Func 𝐸))
100	27	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
101	2, 3, 21, 100, 92	catidcl 16166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
102	1, 2, 3, 98, 99, 92, 92, 101	prf2 16665	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ⟨((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))⟩)
103	1, 2, 3, 98, 99, 92	prf1 16663	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝑃)‘𝑥) = ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩)
104	103	fveq2d 6107	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)) = ((Id‘𝑇)‘⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩))
105	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat)
106	31	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐸 ∈ Cat)
107	16, 105, 106, 17, 18, 90, 94, 22, 37, 42	xpcid 16652	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩) = ⟨((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))⟩)
108	104, 107	eqtrd 2644	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)) = ⟨((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))⟩)
109	97, 102, 108	3eqtr4d 2654	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)))
110		eqid 2610	. . . . . . 7 ⊢ (comp‘𝐷) = (comp‘𝐷)
111	35	3ad2ant1 1075	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
112		simp21 1087	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶))
113		simp22 1088	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶))
114		simp23 1089	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶))
115		simp3l 1082	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
116		simp3r 1083	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
117	2, 3, 23, 110, 111, 112, 113, 114, 115, 116	funcco 16354	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
118		eqid 2610	. . . . . . 7 ⊢ (comp‘𝐸) = (comp‘𝐸)
119	5	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐺 ∈ (𝐶 Func 𝐸))
120	38, 119, 39	sylancr 694	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺))
121	2, 3, 23, 118, 120, 112, 113, 114, 115, 116	funcco 16354	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(⟨((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)⟩(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓)))
122	117, 121	opeq12d 4348	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))⟩ = ⟨(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)), (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(⟨((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)⟩(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))⟩)
123	4	3ad2ant1 1075	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐹 ∈ (𝐶 Func 𝐷))
124	27	3ad2ant1 1075	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat)
125	2, 3, 23, 124, 112, 113, 114, 115, 116	catcocl 16169	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
126	1, 2, 3, 123, 119, 112, 114, 125	prf2 16665	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ⟨((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))⟩)
127	1, 2, 3, 123, 119, 112	prf1 16663	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑥) = ⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩)
128	1, 2, 3, 123, 119, 113	prf1 16663	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑦) = ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩)
129	127, 128	opeq12d 4348	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)⟩ = ⟨⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩, ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩⟩)
130	1, 2, 3, 123, 119, 114	prf1 16663	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑧) = ⟨((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)⟩)
131	129, 130	oveq12d 6567	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (⟨((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)⟩(comp‘𝑇)((1st ‘𝑃)‘𝑧)) = (⟨⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩, ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩⟩(comp‘𝑇)⟨((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)⟩))
132	1, 2, 3, 123, 119, 113, 114, 116	prf2 16665	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝑃)𝑧)‘𝑔) = ⟨((𝑦(2nd ‘𝐹)𝑧)‘𝑔), ((𝑦(2nd ‘𝐺)𝑧)‘𝑔)⟩)
133	1, 2, 3, 123, 119, 112, 113, 115	prf2 16665	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) = ⟨((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)⟩)
134	131, 132, 133	oveq123d 6570	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(⟨((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)⟩(comp‘𝑇)((1st ‘𝑃)‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = (⟨((𝑦(2nd ‘𝐹)𝑧)‘𝑔), ((𝑦(2nd ‘𝐺)𝑧)‘𝑔)⟩(⟨⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)⟩, ⟨((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)⟩⟩(comp‘𝑇)⟨((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)⟩)⟨((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)⟩))
135	36	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
136	135, 112	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
137	41	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐸))
138	137, 112	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸))
139	135, 113	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
140	137, 113	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸))
141	135, 114	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷))
142	137, 114	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑧) ∈ (Base‘𝐸))
143	2, 3, 55, 111, 112, 113	funcf2 16351	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
144	143, 115	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
145	2, 3, 61, 120, 112, 113	funcf2 16351	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
146	145, 115	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))
147	2, 3, 55, 111, 113, 114	funcf2 16351	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
148	147, 116	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
149	2, 3, 61, 120, 113, 114	funcf2 16351	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐺)‘𝑦)(Hom ‘𝐸)((1st ‘𝐺)‘𝑧)))
150	149, 116	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐺)𝑧)‘𝑔) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐸)((1st ‘𝐺)‘𝑧)))
151	16, 17, 18, 55, 61, 136, 138, 139, 140, 110, 118, 24, 141, 142, 144, 146, 148, 150	xpcco2 16650	. . . . . 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 ‘𝐺)𝑦)‘𝑓))⟩)
152	134, 151	eqtrd 2644	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(⟨((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)⟩(comp‘𝑇)((1st ‘𝑃)‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = ⟨(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)), (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(⟨((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)⟩(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))⟩)
153	122, 126, 152	3eqtr4d 2654	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(⟨((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)⟩(comp‘𝑇)((1st ‘𝑃)‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓)))
154	2, 19, 3, 20, 21, 22, 23, 24, 27, 32, 48, 54, 89, 109, 153	isfuncd 16348	. . 3 ⊢ (𝜑 → (1st ‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃))
155		df-br 4584	. . 3 ⊢ ((1st ‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃) ↔ ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩ ∈ (𝐶 Func 𝑇))
156	154, 155	sylib 207	. 2 ⊢ (𝜑 → ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩ ∈ (𝐶 Func 𝑇))
157	15, 156	eqeltrd 2688	1 ⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  Vcvv 3173  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1^st c1st 7057  2^nd c2nd 7058  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148  Idccid 16149   Func cfunc 16337   ×_c cxpc 16631   ⟨,⟩_F cprf 16634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-hom 15793  df-cco 15794  df-cat 16152  df-cid 16153  df-func 16341  df-xpc 16635  df-prf 16638

This theorem is referenced by:  prf1st  16667  prf2nd  16668  uncfcl  16698  uncf1  16699  uncf2  16700  yonedalem1  16735  yonedalem21  16736  yonedalem22  16741