| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prfcl.p | . . . 4
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) | 
| 2 |  | eqid 2737 | . . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 3 |  | eqid 2737 | . . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 4 |  | prfcl.c | . . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) | 
| 5 |  | prfcl.d | . . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) | 
| 6 | 1, 2, 3, 4, 5 | prfval 18244 | . . 3
⊢ (𝜑 → 𝑃 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) | 
| 7 |  | fvex 6919 | . . . . . . 7
⊢
(Base‘𝐶)
∈ V | 
| 8 | 7 | mptex 7243 | . . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) ∈ V | 
| 9 | 7, 7 | mpoex 8104 | . . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) ∈ V | 
| 10 | 8, 9 | op1std 8024 | . . . . 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 8025 | . . . . 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 4881 | . . 3
⊢ (𝜑 → 〈(1st
‘𝑃), (2nd
‘𝑃)〉 =
〈(𝑥 ∈
(Base‘𝐶) ↦
〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) | 
| 15 | 6, 14 | eqtr4d 2780 | . 2
⊢ (𝜑 → 𝑃 = 〈(1st ‘𝑃), (2nd ‘𝑃)〉) | 
| 16 |  | prfcl.t | . . . . 5
⊢ 𝑇 = (𝐷 ×c 𝐸) | 
| 17 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 18 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝐸) =
(Base‘𝐸) | 
| 19 | 16, 17, 18 | xpcbas 18223 | . . . 4
⊢
((Base‘𝐷)
× (Base‘𝐸)) =
(Base‘𝑇) | 
| 20 |  | eqid 2737 | . . . 4
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) | 
| 21 |  | eqid 2737 | . . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) | 
| 22 |  | eqid 2737 | . . . 4
⊢
(Id‘𝑇) =
(Id‘𝑇) | 
| 23 |  | eqid 2737 | . . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) | 
| 24 |  | eqid 2737 | . . . 4
⊢
(comp‘𝑇) =
(comp‘𝑇) | 
| 25 |  | funcrcl 17908 | . . . . . 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 17908 | . . . . . . 7
⊢ (𝐺 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) | 
| 30 | 5, 29 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) | 
| 31 | 30 | simprd 495 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ Cat) | 
| 32 | 16, 28, 31 | xpccat 18235 | . . . 4
⊢ (𝜑 → 𝑇 ∈ Cat) | 
| 33 |  | relfunc 17907 | . . . . . . . . 9
⊢ Rel
(𝐶 Func 𝐷) | 
| 34 |  | 1st2ndbr 8067 | . . . . . . . . 9
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 35 | 33, 4, 34 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 36 | 2, 17, 35 | funcf1 17911 | . . . . . . 7
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 37 | 36 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) | 
| 38 |  | relfunc 17907 | . . . . . . . . 9
⊢ Rel
(𝐶 Func 𝐸) | 
| 39 |  | 1st2ndbr 8067 | . . . . . . . . 9
⊢ ((Rel
(𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) | 
| 40 | 38, 5, 39 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) | 
| 41 | 2, 18, 40 | funcf1 17911 | . . . . . . 7
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(Base‘𝐸)) | 
| 42 | 41 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) | 
| 43 | 37, 42 | opelxpd 5724 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 ∈ ((Base‘𝐷) × (Base‘𝐸))) | 
| 44 | 11, 43 | fmpt3d 7136 | . . . 4
⊢ (𝜑 → (1st
‘𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸))) | 
| 45 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) | 
| 46 |  | ovex 7464 | . . . . . . 7
⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V | 
| 47 | 46 | mptex 7243 | . . . . . 6
⊢ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉) ∈ V | 
| 48 | 45, 47 | fnmpoi 8095 | . . . . 5
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) Fn ((Base‘𝐶) × (Base‘𝐶)) | 
| 49 | 13 | fneq1d 6661 | . . . . 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 7448 | . . . . . 6
⊢ (𝜑 → (𝑥(2nd ‘𝑃)𝑦) = (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))𝑦)) | 
| 52 | 45 | ovmpt4g 7580 | . . . . . . 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 2797 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) | 
| 55 |  | eqid 2737 | . . . . . . . . 9
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 56 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 57 |  | simprl 771 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) | 
| 58 |  | simprr 773 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) | 
| 59 | 2, 3, 55, 56, 57, 58 | funcf2 17913 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 60 | 59 | ffvelcdmda 7104 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐹)𝑦)‘ℎ) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 61 |  | eqid 2737 | . . . . . . . . 9
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) | 
| 62 | 40 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) | 
| 63 | 2, 3, 61, 62, 57, 58 | funcf2 17913 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) | 
| 64 | 63 | ffvelcdmda 7104 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘ℎ) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) | 
| 65 | 60, 64 | opelxpd 5724 | . . . . . 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 18245 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑥) = 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) | 
| 69 | 1, 2, 3, 66, 67, 58 | prf1 18245 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑦) = 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉) | 
| 70 | 68, 69 | oveq12d 7449 | . . . . . . . 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 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) | 
| 74 | 73 | adantrl 716 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) | 
| 75 | 41 | ffvelcdmda 7104 | . . . . . . . . . 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 18231 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(Hom ‘𝑇)〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))) | 
| 78 | 70, 77 | eqtrd 2777 | . . . . . . 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 2844 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉 ∈ (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦))) | 
| 81 | 54, 80 | fmpt3d 7136 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦))) | 
| 82 |  | eqid 2737 | . . . . . . 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 17915 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))) | 
| 86 |  | eqid 2737 | . . . . . . 7
⊢
(Id‘𝐸) =
(Id‘𝐸) | 
| 87 | 40 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) | 
| 88 | 2, 21, 86, 87, 84 | funcid 17915 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))) | 
| 89 | 85, 88 | opeq12d 4881 | . . . . 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 17725 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥)) | 
| 94 | 1, 2, 3, 90, 91, 84, 84, 93 | prf2 18247 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = 〈((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))〉) | 
| 95 | 1, 2, 3, 90, 91, 84 | prf1 18245 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝑃)‘𝑥) = 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) | 
| 96 | 95 | fveq2d 6910 | . . . . . 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 18234 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) = 〈((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))〉) | 
| 100 | 96, 99 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)) = 〈((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))〉) | 
| 101 | 89, 94, 100 | 3eqtr4d 2787 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥))) | 
| 102 |  | eqid 2737 | . . . . . . 7
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 103 | 35 | 3ad2ant1 1134 | . . . . . . 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 17916 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))) | 
| 110 |  | eqid 2737 | . . . . . . 7
⊢
(comp‘𝐸) =
(comp‘𝐸) | 
| 111 | 5 | 3ad2ant1 1134 | . . . . . . . 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 17916 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))) | 
| 114 | 109, 113 | opeq12d 4881 | . . . . 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 1134 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐹 ∈ (𝐶 Func 𝐷)) | 
| 116 | 27 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat) | 
| 117 | 2, 3, 23, 116, 104, 105, 106, 107, 108 | catcocl 17728 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) | 
| 118 | 1, 2, 3, 115, 111, 104, 106, 117 | prf2 18247 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = 〈((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))〉) | 
| 119 | 1, 2, 3, 115, 111, 104 | prf1 18245 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑥) = 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) | 
| 120 | 1, 2, 3, 115, 111, 105 | prf1 18245 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑦) = 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉) | 
| 121 | 119, 120 | opeq12d 4881 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 〈((1st
‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)〉 = 〈〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉, 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉〉) | 
| 122 | 1, 2, 3, 115, 111, 106 | prf1 18245 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑧) = 〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉) | 
| 123 | 121, 122 | oveq12d 7449 | . . . . . . 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 18247 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝑃)𝑧)‘𝑔) = 〈((𝑦(2nd ‘𝐹)𝑧)‘𝑔), ((𝑦(2nd ‘𝐺)𝑧)‘𝑔)〉) | 
| 125 | 1, 2, 3, 115, 111, 104, 105, 107 | prf2 18247 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) = 〈((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)〉) | 
| 126 | 123, 124,
125 | oveq123d 7452 | . . . . . 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 1134 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 128 | 127, 104 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) | 
| 129 | 41 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐸)) | 
| 130 | 129, 104 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) | 
| 131 | 127, 105 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) | 
| 132 | 129, 105 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸)) | 
| 133 | 127, 106 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷)) | 
| 134 | 129, 106 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑧) ∈ (Base‘𝐸)) | 
| 135 | 2, 3, 55, 103, 104, 105 | funcf2 17913 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 136 | 135, 107 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 137 | 2, 3, 61, 112, 104, 105 | funcf2 17913 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) | 
| 138 | 137, 107 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) | 
| 139 | 2, 3, 55, 103, 105, 106 | funcf2 17913 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) | 
| 140 | 139, 108 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) | 
| 141 | 2, 3, 61, 112, 105, 106 | funcf2 17913 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐺)‘𝑦)(Hom ‘𝐸)((1st ‘𝐺)‘𝑧))) | 
| 142 | 141, 108 | ffvelcdmd 7105 | . . . . . . 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 18232 | . . . . . 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 2777 | . . . . 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 2787 | . . . 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 17910 | . . 3
⊢ (𝜑 → (1st
‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃)) | 
| 147 |  | df-br 5144 | . . 3
⊢
((1st ‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃) ↔ 〈(1st ‘𝑃), (2nd ‘𝑃)〉 ∈ (𝐶 Func 𝑇)) | 
| 148 | 146, 147 | sylib 218 | . 2
⊢ (𝜑 → 〈(1st
‘𝑃), (2nd
‘𝑃)〉 ∈
(𝐶 Func 𝑇)) | 
| 149 | 15, 148 | eqeltrd 2841 | 1
⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇)) |