| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hofcl.m | . . . 4
⊢ 𝑀 =
(HomF‘𝐶) | 
| 2 |  | hofcl.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 3 |  | eqid 2736 | . . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 4 |  | eqid 2736 | . . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 5 |  | eqid 2736 | . . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) | 
| 6 | 1, 2, 3, 4, 5 | hofval 18298 | . . 3
⊢ (𝜑 → 𝑀 = 〈(Homf
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉) | 
| 7 |  | fvex 6918 | . . . . . 6
⊢
(Homf ‘𝐶) ∈ V | 
| 8 |  | fvex 6918 | . . . . . . . 8
⊢
(Base‘𝐶)
∈ V | 
| 9 | 8, 8 | xpex 7774 | . . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐶))
∈ V | 
| 10 | 9, 9 | mpoex 8105 | . . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) ∈ V | 
| 11 | 7, 10 | op2ndd 8026 | . . . . 5
⊢ (𝑀 = 〈(Homf
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉 → (2nd
‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))) | 
| 12 | 6, 11 | syl 17 | . . . 4
⊢ (𝜑 → (2nd
‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))) | 
| 13 | 12 | opeq2d 4879 | . . 3
⊢ (𝜑 →
〈(Homf ‘𝐶), (2nd ‘𝑀)〉 = 〈(Homf
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉) | 
| 14 | 6, 13 | eqtr4d 2779 | . 2
⊢ (𝜑 → 𝑀 = 〈(Homf
‘𝐶), (2nd
‘𝑀)〉) | 
| 15 |  | eqid 2736 | . . . . 5
⊢ (𝑂 ×c
𝐶) = (𝑂 ×c 𝐶) | 
| 16 |  | hofcl.o | . . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) | 
| 17 | 16, 3 | oppcbas 17762 | . . . . 5
⊢
(Base‘𝐶) =
(Base‘𝑂) | 
| 18 | 15, 17, 3 | xpcbas 18224 | . . . 4
⊢
((Base‘𝐶)
× (Base‘𝐶)) =
(Base‘(𝑂
×c 𝐶)) | 
| 19 |  | eqid 2736 | . . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 20 |  | eqid 2736 | . . . 4
⊢ (Hom
‘(𝑂
×c 𝐶)) = (Hom ‘(𝑂 ×c 𝐶)) | 
| 21 |  | eqid 2736 | . . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 22 |  | eqid 2736 | . . . 4
⊢
(Id‘(𝑂
×c 𝐶)) = (Id‘(𝑂 ×c 𝐶)) | 
| 23 |  | eqid 2736 | . . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) | 
| 24 |  | eqid 2736 | . . . 4
⊢
(comp‘(𝑂
×c 𝐶)) = (comp‘(𝑂 ×c 𝐶)) | 
| 25 |  | eqid 2736 | . . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 26 | 16 | oppccat 17766 | . . . . . 6
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) | 
| 27 | 2, 26 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑂 ∈ Cat) | 
| 28 | 15, 27, 2 | xpccat 18236 | . . . 4
⊢ (𝜑 → (𝑂 ×c 𝐶) ∈ Cat) | 
| 29 |  | hofcl.u | . . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) | 
| 30 |  | hofcl.d | . . . . . 6
⊢ 𝐷 = (SetCat‘𝑈) | 
| 31 | 30 | setccat 18131 | . . . . 5
⊢ (𝑈 ∈ 𝑉 → 𝐷 ∈ Cat) | 
| 32 | 29, 31 | syl 17 | . . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) | 
| 33 |  | eqid 2736 | . . . . . . . 8
⊢
(Homf ‘𝐶) = (Homf ‘𝐶) | 
| 34 | 33, 3 | homffn 17737 | . . . . . . 7
⊢
(Homf ‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) | 
| 35 | 34 | a1i 11 | . . . . . 6
⊢ (𝜑 → (Homf
‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) | 
| 36 |  | hofcl.h | . . . . . 6
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ 𝑈) | 
| 37 |  | df-f 6564 | . . . . . 6
⊢
((Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ ((Homf
‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ∧ ran
(Homf ‘𝐶) ⊆ 𝑈)) | 
| 38 | 35, 36, 37 | sylanbrc 583 | . . . . 5
⊢ (𝜑 → (Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) | 
| 39 | 30, 29 | setcbas 18124 | . . . . . 6
⊢ (𝜑 → 𝑈 = (Base‘𝐷)) | 
| 40 | 39 | feq3d 6722 | . . . . 5
⊢ (𝜑 → ((Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ (Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷))) | 
| 41 | 38, 40 | mpbid 232 | . . . 4
⊢ (𝜑 → (Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷)) | 
| 42 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) | 
| 43 |  | ovex 7465 | . . . . . . 7
⊢
((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∈ V | 
| 44 |  | ovex 7465 | . . . . . . 7
⊢
((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ∈ V | 
| 45 | 43, 44 | mpoex 8105 | . . . . . 6
⊢ (𝑓 ∈ ((1st
‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) ∈ V | 
| 46 | 42, 45 | fnmpoi 8096 | . . . . 5
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))) | 
| 47 | 12 | fneq1d 6660 | . . . . 5
⊢ (𝜑 → ((2nd
‘𝑀) Fn
(((Base‘𝐶) ×
(Base‘𝐶)) ×
((Base‘𝐶) ×
(Base‘𝐶))) ↔
(𝑥 ∈
((Base‘𝐶) ×
(Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))))) | 
| 48 | 46, 47 | mpbiri 258 | . . . 4
⊢ (𝜑 → (2nd
‘𝑀) Fn
(((Base‘𝐶) ×
(Base‘𝐶)) ×
((Base‘𝐶) ×
(Base‘𝐶)))) | 
| 49 | 2 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat) | 
| 50 |  | simplrr 777 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) | 
| 51 |  | xp1st 8047 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑦) ∈
(Base‘𝐶)) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (1st ‘𝑦) ∈ (Base‘𝐶)) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑦) ∈ (Base‘𝐶)) | 
| 54 |  | simplrl 776 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) | 
| 55 |  | xp1st 8047 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑥) ∈
(Base‘𝐶)) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (1st ‘𝑥) ∈ (Base‘𝐶)) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑥) ∈ (Base‘𝐶)) | 
| 58 |  | xp2nd 8048 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑦) ∈
(Base‘𝐶)) | 
| 59 | 50, 58 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (2nd ‘𝑦) ∈ (Base‘𝐶)) | 
| 60 | 59 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑦) ∈ (Base‘𝐶)) | 
| 61 |  | simplrl 776 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))) | 
| 62 |  | 1st2nd2 8054 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 63 | 54, 62 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 65 | 64 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2nd ‘𝑦)) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))) | 
| 66 | 65 | oveqd 7449 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) = (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))ℎ)) | 
| 67 |  | xp2nd 8048 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑥) ∈
(Base‘𝐶)) | 
| 68 | 54, 67 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) | 
| 69 | 68 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑥) ∈ (Base‘𝐶)) | 
| 70 | 63 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 71 |  | df-ov 7435 | . . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) = ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 72 | 70, 71 | eqtr4di 2794 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 73 | 72 | eleq2d 2826 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↔ ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))) | 
| 74 | 73 | biimpa 476 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 75 |  | simplrr 777 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 76 | 3, 4, 5, 49, 57, 69, 60, 74, 75 | catcocl 17729 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 77 | 66, 76 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 78 | 3, 4, 5, 49, 53, 57, 60, 61, 77 | catcocl 17729 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓) ∈ ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 79 |  | 1st2nd2 8054 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 80 | 50, 79 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 81 | 80 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 82 |  | df-ov 7435 | . . . . . . . . . . . . 13
⊢
((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)) = ((Hom ‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 83 | 81, 82 | eqtr4di 2794 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 84 | 83 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((Hom ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 85 | 78, 84 | eleqtrrd 2843 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓) ∈ ((Hom ‘𝐶)‘𝑦)) | 
| 86 | 85 | fmpttd 7134 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦)) | 
| 87 | 29 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑈 ∈ 𝑉) | 
| 88 | 33, 3, 4, 56, 68 | homfval 17736 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((1st ‘𝑥)(Homf
‘𝐶)(2nd
‘𝑥)) =
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 89 | 63 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 90 |  | df-ov 7435 | . . . . . . . . . . . . 13
⊢
((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 91 | 89, 90 | eqtr4di 2794 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥))) | 
| 92 | 88, 91, 72 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘𝑥)) | 
| 93 | 38 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) | 
| 94 | 93, 54 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) ∈ 𝑈) | 
| 95 | 92, 94 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) ∈ 𝑈) | 
| 96 | 33, 3, 4, 52, 59 | homfval 17736 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((1st ‘𝑦)(Homf
‘𝐶)(2nd
‘𝑦)) =
((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 97 | 80 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) = ((Homf
‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 98 |  | df-ov 7435 | . . . . . . . . . . . . 13
⊢
((1st ‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦)) = ((Homf
‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 99 | 97, 98 | eqtr4di 2794 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) = ((1st
‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦))) | 
| 100 | 96, 99, 83 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘𝑦)) | 
| 101 | 93, 50 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) ∈ 𝑈) | 
| 102 | 100, 101 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) ∈ 𝑈) | 
| 103 | 30, 87, 21, 95, 102 | elsetchom 18127 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)) ↔ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦))) | 
| 104 | 86, 103 | mpbird 257 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦))) | 
| 105 | 92, 100 | oveq12d 7450 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) = (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦))) | 
| 106 | 104, 105 | eleqtrrd 2843 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) | 
| 107 | 106 | ralrimivva 3201 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ∀𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))∀𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) | 
| 108 |  | eqid 2736 | . . . . . . 7
⊢ (𝑓 ∈ ((1st
‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) | 
| 109 | 108 | fmpo 8094 | . . . . . 6
⊢
(∀𝑓 ∈
((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))∀𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) | 
| 110 | 107, 109 | sylib 218 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) | 
| 111 | 12 | oveqd 7449 | . . . . . . 7
⊢ (𝜑 → (𝑥(2nd ‘𝑀)𝑦) = (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦)) | 
| 112 | 42 | ovmpt4g 7581 | . . . . . . . 8
⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) ∈ V) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) | 
| 113 | 45, 112 | mp3an3 1451 | . . . . . . 7
⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) | 
| 114 | 111, 113 | sylan9eq 2796 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd ‘𝑀)𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) | 
| 115 |  | eqid 2736 | . . . . . . . 8
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) | 
| 116 |  | simprl 770 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) | 
| 117 |  | simprr 772 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) | 
| 118 | 15, 18, 115, 4, 20, 116, 117 | xpchom 18226 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 119 | 4, 16 | oppchom 17759 | . . . . . . . 8
⊢
((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) = ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) | 
| 120 | 119 | xpeq1i 5710 | . . . . . . 7
⊢
(((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) = (((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 121 | 118, 120 | eqtrdi 2792 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 122 | 114, 121 | feq12d 6723 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((𝑥(2nd ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)))) | 
| 123 | 110, 122 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) | 
| 124 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Id‘𝐶) =
(Id‘𝐶) | 
| 125 | 2 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → 𝐶 ∈ Cat) | 
| 126 | 55 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st ‘𝑥) ∈ (Base‘𝐶)) | 
| 127 | 126 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (1st ‘𝑥) ∈ (Base‘𝐶)) | 
| 128 | 67 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) | 
| 129 | 128 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) | 
| 130 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 131 | 3, 4, 124, 125, 127, 5, 129, 130 | catlid 17727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓) = 𝑓) | 
| 132 | 131 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = (𝑓(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥)))) | 
| 133 | 3, 4, 124, 125, 127, 5, 129, 130 | catrid 17728 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (𝑓(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = 𝑓) | 
| 134 | 132, 133 | eqtrd 2776 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = 𝑓) | 
| 135 | 134 | mpteq2dva 5241 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥)))) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓)) | 
| 136 |  | df-ov 7435 | . . . . . . 7
⊢
(((Id‘𝐶)‘(1st ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)((Id‘𝐶)‘(2nd ‘𝑥))) = ((〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉) | 
| 137 | 2 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝐶 ∈ Cat) | 
| 138 | 3, 4, 124, 137, 126 | catidcl 17726 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(1st ‘𝑥)) ∈ ((1st
‘𝑥)(Hom ‘𝐶)(1st ‘𝑥))) | 
| 139 | 3, 4, 124, 137, 128 | catidcl 17726 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(2nd ‘𝑥)) ∈ ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 140 | 1, 137, 3, 4, 126, 128, 126, 128, 5, 138, 139 | hof2val 18302 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((Id‘𝐶)‘(1st ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)((Id‘𝐶)‘(2nd ‘𝑥))) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))))) | 
| 141 | 136, 140 | eqtr3id 2790 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))))) | 
| 142 | 62 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 143 | 142 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 144 | 143, 90 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥))) | 
| 145 | 33, 3, 4, 126, 128 | homfval 17736 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((1st ‘𝑥)(Homf
‘𝐶)(2nd
‘𝑥)) =
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 146 | 144, 145 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 147 | 146 | reseq2d 5996 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Homf ‘𝐶)‘𝑥)) = ( I ↾ ((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))) | 
| 148 |  | mptresid 6068 | . . . . . . 7
⊢ ( I
↾ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓) | 
| 149 | 147, 148 | eqtrdi 2792 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Homf ‘𝐶)‘𝑥)) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓)) | 
| 150 | 135, 141,
149 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉) = ( I ↾
((Homf ‘𝐶)‘𝑥))) | 
| 151 | 142, 142 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(2nd ‘𝑀)𝑥) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 152 | 142 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = ((Id‘(𝑂 ×c 𝐶))‘〈(1st
‘𝑥), (2nd
‘𝑥)〉)) | 
| 153 | 27 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑂 ∈ Cat) | 
| 154 |  | eqid 2736 | . . . . . . . 8
⊢
(Id‘𝑂) =
(Id‘𝑂) | 
| 155 | 15, 153, 137, 17, 3, 154, 124, 22, 126, 128 | xpcid 18235 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘〈(1st
‘𝑥), (2nd
‘𝑥)〉) =
〈((Id‘𝑂)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))〉) | 
| 156 | 16, 124 | oppcid 17765 | . . . . . . . . . 10
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) =
(Id‘𝐶)) | 
| 157 | 137, 156 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (Id‘𝑂) = (Id‘𝐶)) | 
| 158 | 157 | fveq1d 6907 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝑂)‘(1st ‘𝑥)) = ((Id‘𝐶)‘(1st
‘𝑥))) | 
| 159 | 158 | opeq1d 4878 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 〈((Id‘𝑂)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉 =
〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))〉) | 
| 160 | 152, 155,
159 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = 〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))〉) | 
| 161 | 151, 160 | fveq12d 6912 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd ‘𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑥), (2nd ‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉)) | 
| 162 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑈 ∈ 𝑉) | 
| 163 | 38 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) ∈ 𝑈) | 
| 164 | 30, 23, 162, 163 | setcid 18132 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐷)‘((Homf
‘𝐶)‘𝑥)) = ( I ↾
((Homf ‘𝐶)‘𝑥))) | 
| 165 | 150, 161,
164 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd ‘𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((Homf
‘𝐶)‘𝑥))) | 
| 166 | 2 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat) | 
| 167 | 29 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑈 ∈ 𝑉) | 
| 168 | 36 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ran (Homf
‘𝐶) ⊆ 𝑈) | 
| 169 |  | simp21 1206 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) | 
| 170 | 169, 55 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑥) ∈ (Base‘𝐶)) | 
| 171 | 169, 67 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) | 
| 172 |  | simp22 1207 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) | 
| 173 | 172, 51 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑦) ∈ (Base‘𝐶)) | 
| 174 | 172, 58 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑦) ∈ (Base‘𝐶)) | 
| 175 |  | simp23 1208 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) | 
| 176 |  | xp1st 8047 | . . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑧) ∈
(Base‘𝐶)) | 
| 177 | 175, 176 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑧) ∈ (Base‘𝐶)) | 
| 178 |  | xp2nd 8048 | . . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑧) ∈
(Base‘𝐶)) | 
| 179 | 175, 178 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑧) ∈ (Base‘𝐶)) | 
| 180 |  | simp3l 1201 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)) | 
| 181 | 15, 18, 115, 4, 20, 169, 172 | xpchom 18226 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 182 | 180, 181 | eleqtrd 2842 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 183 |  | xp1st 8047 | . . . . . . . 8
⊢ (𝑓 ∈ (((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → (1st
‘𝑓) ∈
((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦))) | 
| 184 | 182, 183 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑓) ∈ ((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦))) | 
| 185 | 184, 119 | eleqtrdi 2850 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑓) ∈ ((1st
‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))) | 
| 186 |  | xp2nd 8048 | . . . . . . 7
⊢ (𝑓 ∈ (((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → (2nd
‘𝑓) ∈
((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 187 | 182, 186 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑓) ∈ ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 188 |  | simp3r 1202 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧)) | 
| 189 | 15, 18, 115, 4, 20, 172, 175 | xpchom 18226 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧) = (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 190 | 188, 189 | eleqtrd 2842 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 191 |  | xp1st 8047 | . . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → (1st
‘𝑔) ∈
((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧))) | 
| 192 | 190, 191 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑔) ∈ ((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧))) | 
| 193 | 4, 16 | oppchom 17759 | . . . . . . 7
⊢
((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) = ((1st ‘𝑧)(Hom ‘𝐶)(1st ‘𝑦)) | 
| 194 | 192, 193 | eleqtrdi 2850 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑔) ∈ ((1st
‘𝑧)(Hom ‘𝐶)(1st ‘𝑦))) | 
| 195 |  | xp2nd 8048 | . . . . . . 7
⊢ (𝑔 ∈ (((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → (2nd
‘𝑔) ∈
((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) | 
| 196 | 190, 195 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) | 
| 197 | 1, 16, 30, 166, 167, 168, 3, 4, 170, 171, 173, 174, 177, 179, 185, 187, 194, 196 | hofcllem 18304 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))) = (((1st
‘𝑔)(〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)(2nd
‘𝑔))(〈((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))((1st ‘𝑓)(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)(2nd
‘𝑓)))) | 
| 198 | 169, 62 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 199 |  | 1st2nd2 8054 | . . . . . . . . 9
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 200 | 175, 199 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 201 | 198, 200 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝑀)𝑧) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 202 | 172, 79 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 203 | 198, 202 | opeq12d 4880 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 〈𝑥, 𝑦〉 = 〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉) | 
| 204 | 203, 200 | oveq12d 7450 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧) = (〈〈(1st ‘𝑥), (2nd ‘𝑥)〉, 〈(1st
‘𝑦), (2nd
‘𝑦)〉〉(comp‘(𝑂 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)) | 
| 205 |  | 1st2nd2 8054 | . . . . . . . . . 10
⊢ (𝑔 ∈ (((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) | 
| 206 | 190, 205 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) | 
| 207 |  | 1st2nd2 8054 | . . . . . . . . . 10
⊢ (𝑓 ∈ (((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) | 
| 208 | 182, 207 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) | 
| 209 | 204, 206,
208 | oveq123d 7453 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓) = (〈(1st ‘𝑔), (2nd ‘𝑔)〉(〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉(comp‘(𝑂 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)〈(1st ‘𝑓), (2nd ‘𝑓)〉)) | 
| 210 |  | eqid 2736 | . . . . . . . . 9
⊢
(comp‘𝑂) =
(comp‘𝑂) | 
| 211 | 15, 17, 3, 115, 4, 170, 171, 173, 174, 210, 5, 24, 177, 179, 184, 187, 192, 196 | xpcco2 18233 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (〈(1st
‘𝑔), (2nd
‘𝑔)〉(〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉(comp‘(𝑂 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)〈(1st ‘𝑓), (2nd ‘𝑓)〉) =
〈((1st ‘𝑔)(〈(1st ‘𝑥), (1st ‘𝑦)〉(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) | 
| 212 | 3, 5, 16, 170, 173, 177 | oppcco 17761 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑔)(〈(1st
‘𝑥), (1st
‘𝑦)〉(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)) = ((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))) | 
| 213 | 212 | opeq1d 4878 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 〈((1st
‘𝑔)(〈(1st ‘𝑥), (1st ‘𝑦)〉(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉 =
〈((1st ‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) | 
| 214 | 209, 211,
213 | 3eqtrd 2780 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓) = 〈((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd ‘𝑔)(〈(2nd
‘𝑥), (2nd
‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) | 
| 215 | 201, 214 | fveq12d 6912 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈((1st
‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉)) | 
| 216 |  | df-ov 7435 | . . . . . 6
⊢
(((1st ‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)((2nd ‘𝑔)(〈(2nd
‘𝑥), (2nd
‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈((1st
‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) | 
| 217 | 215, 216 | eqtr4di 2794 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = (((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓)))) | 
| 218 | 198 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑥) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 219 | 218, 90 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥))) | 
| 220 | 33, 3, 4, 170, 171 | homfval 17736 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑥)(Homf
‘𝐶)(2nd
‘𝑥)) =
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 221 | 219, 220 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) | 
| 222 | 202 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑦) = ((Homf
‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 223 | 222, 98 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑦) = ((1st
‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦))) | 
| 224 | 33, 3, 4, 173, 174 | homfval 17736 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑦)(Homf
‘𝐶)(2nd
‘𝑦)) =
((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 225 | 223, 224 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑦) = ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) | 
| 226 | 221, 225 | opeq12d 4880 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 〈((Homf
‘𝐶)‘𝑥), ((Homf
‘𝐶)‘𝑦)〉 = 〈((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉) | 
| 227 | 200 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑧) = ((Homf
‘𝐶)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 228 |  | df-ov 7435 | . . . . . . . . 9
⊢
((1st ‘𝑧)(Homf ‘𝐶)(2nd ‘𝑧)) = ((Homf
‘𝐶)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 229 | 227, 228 | eqtr4di 2794 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑧) = ((1st
‘𝑧)(Homf ‘𝐶)(2nd ‘𝑧))) | 
| 230 | 33, 3, 4, 177, 179 | homfval 17736 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑧)(Homf
‘𝐶)(2nd
‘𝑧)) =
((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧))) | 
| 231 | 229, 230 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑧) = ((1st
‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧))) | 
| 232 | 226, 231 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (〈((Homf
‘𝐶)‘𝑥), ((Homf
‘𝐶)‘𝑦)〉(comp‘𝐷)((Homf
‘𝐶)‘𝑧)) = (〈((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 233 | 202, 200 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(2nd ‘𝑀)𝑧) = (〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 234 | 233, 206 | fveq12d 6912 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝑀)𝑧)‘𝑔) = ((〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)) | 
| 235 |  | df-ov 7435 | . . . . . . 7
⊢
((1st ‘𝑔)(〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)(2nd
‘𝑔)) =
((〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉) | 
| 236 | 234, 235 | eqtr4di 2794 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝑀)𝑧)‘𝑔) = ((1st ‘𝑔)(〈(1st
‘𝑦), (2nd
‘𝑦)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)(2nd ‘𝑔))) | 
| 237 | 198, 202 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝑀)𝑦) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 238 | 237, 208 | fveq12d 6912 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑦)‘𝑓) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)‘〈(1st
‘𝑓), (2nd
‘𝑓)〉)) | 
| 239 |  | df-ov 7435 | . . . . . . 7
⊢
((1st ‘𝑓)(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)(2nd
‘𝑓)) =
((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑦), (2nd
‘𝑦)〉)‘〈(1st
‘𝑓), (2nd
‘𝑓)〉) | 
| 240 | 238, 239 | eqtr4di 2794 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑦)‘𝑓) = ((1st ‘𝑓)(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑦), (2nd
‘𝑦)〉)(2nd ‘𝑓))) | 
| 241 | 232, 236,
240 | oveq123d 7453 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (((𝑦(2nd ‘𝑀)𝑧)‘𝑔)(〈((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)〉(comp‘𝐷)((Homf ‘𝐶)‘𝑧))((𝑥(2nd ‘𝑀)𝑦)‘𝑓)) = (((1st ‘𝑔)(〈(1st
‘𝑦), (2nd
‘𝑦)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)(2nd ‘𝑔))(〈((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))((1st ‘𝑓)(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)(2nd
‘𝑓)))) | 
| 242 | 197, 217,
241 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = (((𝑦(2nd ‘𝑀)𝑧)‘𝑔)(〈((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)〉(comp‘𝐷)((Homf ‘𝐶)‘𝑧))((𝑥(2nd ‘𝑀)𝑦)‘𝑓))) | 
| 243 | 18, 19, 20, 21, 22, 23, 24, 25, 28, 32, 41, 48, 123, 165, 242 | isfuncd 17911 | . . 3
⊢ (𝜑 → (Homf
‘𝐶)((𝑂 ×c
𝐶) Func 𝐷)(2nd ‘𝑀)) | 
| 244 |  | df-br 5143 | . . 3
⊢
((Homf ‘𝐶)((𝑂 ×c 𝐶) Func 𝐷)(2nd ‘𝑀) ↔ 〈(Homf
‘𝐶), (2nd
‘𝑀)〉 ∈
((𝑂
×c 𝐶) Func 𝐷)) | 
| 245 | 243, 244 | sylib 218 | . 2
⊢ (𝜑 →
〈(Homf ‘𝐶), (2nd ‘𝑀)〉 ∈ ((𝑂 ×c 𝐶) Func 𝐷)) | 
| 246 | 14, 245 | eqeltrd 2840 | 1
⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷)) |