MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hofcl Structured version   Visualization version   GIF version

Theorem hofcl 17767
Description: Closure of the Hom functor. Note that the codomain is the category SetCat‘𝑈 for any universe 𝑈 which contains each Hom-set. This corresponds to the assertion that 𝐶 be locally small (with respect to 𝑈). (Contributed by Mario Carneiro, 15-Jan-2017.)
Hypotheses
Ref Expression
hofcl.m 𝑀 = (HomF𝐶)
hofcl.o 𝑂 = (oppCat‘𝐶)
hofcl.d 𝐷 = (SetCat‘𝑈)
hofcl.c (𝜑𝐶 ∈ Cat)
hofcl.u (𝜑𝑈𝑉)
hofcl.h (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
Assertion
Ref Expression
hofcl (𝜑𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷))

Proof of Theorem hofcl
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofcl.m . . . 4 𝑀 = (HomF𝐶)
2 hofcl.c . . . 4 (𝜑𝐶 ∈ Cat)
3 eqid 2737 . . . 4 (Base‘𝐶) = (Base‘𝐶)
4 eqid 2737 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
5 eqid 2737 . . . 4 (comp‘𝐶) = (comp‘𝐶)
61, 2, 3, 4, 5hofval 17760 . . 3 (𝜑𝑀 = ⟨(Homf𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓))))⟩)
7 fvex 6730 . . . . . 6 (Homf𝐶) ∈ V
8 fvex 6730 . . . . . . . 8 (Base‘𝐶) ∈ V
98, 8xpex 7538 . . . . . . 7 ((Base‘𝐶) × (Base‘𝐶)) ∈ V
109, 9mpoex 7850 . . . . . 6 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)))) ∈ V
117, 10op2ndd 7772 . . . . 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𝑦))𝑓)))))
126, 11syl 17 . . . 4 (𝜑 → (2nd𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)))))
1312opeq2d 4791 . . 3 (𝜑 → ⟨(Homf𝐶), (2nd𝑀)⟩ = ⟨(Homf𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓))))⟩)
146, 13eqtr4d 2780 . 2 (𝜑𝑀 = ⟨(Homf𝐶), (2nd𝑀)⟩)
15 eqid 2737 . . . . 5 (𝑂 ×c 𝐶) = (𝑂 ×c 𝐶)
16 hofcl.o . . . . . 6 𝑂 = (oppCat‘𝐶)
1716, 3oppcbas 17222 . . . . 5 (Base‘𝐶) = (Base‘𝑂)
1815, 17, 3xpcbas 17685 . . . 4 ((Base‘𝐶) × (Base‘𝐶)) = (Base‘(𝑂 ×c 𝐶))
19 eqid 2737 . . . 4 (Base‘𝐷) = (Base‘𝐷)
20 eqid 2737 . . . 4 (Hom ‘(𝑂 ×c 𝐶)) = (Hom ‘(𝑂 ×c 𝐶))
21 eqid 2737 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
22 eqid 2737 . . . 4 (Id‘(𝑂 ×c 𝐶)) = (Id‘(𝑂 ×c 𝐶))
23 eqid 2737 . . . 4 (Id‘𝐷) = (Id‘𝐷)
24 eqid 2737 . . . 4 (comp‘(𝑂 ×c 𝐶)) = (comp‘(𝑂 ×c 𝐶))
25 eqid 2737 . . . 4 (comp‘𝐷) = (comp‘𝐷)
2616oppccat 17226 . . . . . 6 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
272, 26syl 17 . . . . 5 (𝜑𝑂 ∈ Cat)
2815, 27, 2xpccat 17697 . . . 4 (𝜑 → (𝑂 ×c 𝐶) ∈ Cat)
29 hofcl.u . . . . 5 (𝜑𝑈𝑉)
30 hofcl.d . . . . . 6 𝐷 = (SetCat‘𝑈)
3130setccat 17591 . . . . 5 (𝑈𝑉𝐷 ∈ Cat)
3229, 31syl 17 . . . 4 (𝜑𝐷 ∈ Cat)
33 eqid 2737 . . . . . . . 8 (Homf𝐶) = (Homf𝐶)
3433, 3homffn 17196 . . . . . . 7 (Homf𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))
3534a1i 11 . . . . . 6 (𝜑 → (Homf𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))
36 hofcl.h . . . . . 6 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
37 df-f 6384 . . . . . 6 ((Homf𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ ((Homf𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ran (Homf𝐶) ⊆ 𝑈))
3835, 36, 37sylanbrc 586 . . . . 5 (𝜑 → (Homf𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈)
3930, 29setcbas 17584 . . . . . 6 (𝜑𝑈 = (Base‘𝐷))
4039feq3d 6532 . . . . 5 (𝜑 → ((Homf𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ (Homf𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷)))
4138, 40mpbid 235 . . . 4 (𝜑 → (Homf𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷))
42 eqid 2737 . . . . . 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 7246 . . . . . . 7 ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∈ V
44 ovex 7246 . . . . . . 7 ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ∈ V
4543, 44mpoex 7850 . . . . . 6 (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓))) ∈ V
4642, 45fnmpoi 7840 . . . . 5 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶)))
4712fneq1d 6472 . . . . 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‘𝐶)))))
4846, 47mpbiri 261 . . . 4 (𝜑 → (2nd𝑀) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))))
492ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat)
50 simplrr 778 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))
51 xp1st 7793 . . . . . . . . . . . . . 14 (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st𝑦) ∈ (Base‘𝐶))
5250, 51syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → (1st𝑦) ∈ (Base‘𝐶))
5352adantr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st𝑦) ∈ (Base‘𝐶))
54 simplrl 777 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)))
55 xp1st 7793 . . . . . . . . . . . . . 14 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st𝑥) ∈ (Base‘𝐶))
5654, 55syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → (1st𝑥) ∈ (Base‘𝐶))
5756adantr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st𝑥) ∈ (Base‘𝐶))
58 xp2nd 7794 . . . . . . . . . . . . . 14 (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd𝑦) ∈ (Base‘𝐶))
5950, 58syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → (2nd𝑦) ∈ (Base‘𝐶))
6059adantr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd𝑦) ∈ (Base‘𝐶))
61 simplrl 777 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)))
62 1st2nd2 7800 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6354, 62syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6463adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6564oveq1d 7228 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2nd𝑦)) = (⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑦)))
6665oveqd 7230 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd𝑦))) = (𝑔(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑦))))
67 xp2nd 7794 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd𝑥) ∈ (Base‘𝐶))
6854, 67syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → (2nd𝑥) ∈ (Base‘𝐶))
6968adantr 484 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd𝑥) ∈ (Base‘𝐶))
7063fveq2d 6721 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩))
71 df-ov 7216 . . . . . . . . . . . . . . . . 17 ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)) = ((Hom ‘𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩)
7270, 71eqtr4di 2796 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
7372eleq2d 2823 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ( ∈ ((Hom ‘𝐶)‘𝑥) ↔ ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))))
7473biimpa 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
75 simplrr 778 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))
763, 4, 5, 49, 57, 69, 60, 74, 75catcocl 17188 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑦))) ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑦)))
7766, 76eqeltrd 2838 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd𝑦))) ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑦)))
783, 4, 5, 49, 53, 57, 60, 61, 77catcocl 17188 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓) ∈ ((1st𝑦)(Hom ‘𝐶)(2nd𝑦)))
79 1st2nd2 7800 . . . . . . . . . . . . . . 15 (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
8050, 79syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
8180fveq2d 6721 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘⟨(1st𝑦), (2nd𝑦)⟩))
82 df-ov 7216 . . . . . . . . . . . . 13 ((1st𝑦)(Hom ‘𝐶)(2nd𝑦)) = ((Hom ‘𝐶)‘⟨(1st𝑦), (2nd𝑦)⟩)
8381, 82eqtr4di 2796 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((1st𝑦)(Hom ‘𝐶)(2nd𝑦)))
8483adantr 484 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ((Hom ‘𝐶)‘𝑦) = ((1st𝑦)(Hom ‘𝐶)(2nd𝑦)))
8578, 84eleqtrrd 2841 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓) ∈ ((Hom ‘𝐶)‘𝑦))
8685fmpttd 6932 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦))
8729ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → 𝑈𝑉)
8833, 3, 4, 56, 68homfval 17195 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((1st𝑥)(Homf𝐶)(2nd𝑥)) = ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
8963fveq2d 6721 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑥) = ((Homf𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩))
90 df-ov 7216 . . . . . . . . . . . . 13 ((1st𝑥)(Homf𝐶)(2nd𝑥)) = ((Homf𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩)
9189, 90eqtr4di 2796 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑥) = ((1st𝑥)(Homf𝐶)(2nd𝑥)))
9288, 91, 723eqtr4d 2787 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑥) = ((Hom ‘𝐶)‘𝑥))
9338ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → (Homf𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈)
9493, 54ffvelrnd 6905 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑥) ∈ 𝑈)
9592, 94eqeltrrd 2839 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑥) ∈ 𝑈)
9633, 3, 4, 52, 59homfval 17195 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((1st𝑦)(Homf𝐶)(2nd𝑦)) = ((1st𝑦)(Hom ‘𝐶)(2nd𝑦)))
9780fveq2d 6721 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑦) = ((Homf𝐶)‘⟨(1st𝑦), (2nd𝑦)⟩))
98 df-ov 7216 . . . . . . . . . . . . 13 ((1st𝑦)(Homf𝐶)(2nd𝑦)) = ((Homf𝐶)‘⟨(1st𝑦), (2nd𝑦)⟩)
9997, 98eqtr4di 2796 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑦) = ((1st𝑦)(Homf𝐶)(2nd𝑦)))
10096, 99, 833eqtr4d 2787 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑦) = ((Hom ‘𝐶)‘𝑦))
10193, 50ffvelrnd 6905 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Homf𝐶)‘𝑦) ∈ 𝑈)
102100, 101eqeltrrd 2839 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑦) ∈ 𝑈)
10330, 87, 21, 95, 102elsetchom 17587 . . . . . . . . 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 ‘𝐶)‘𝑦)))
10486, 103mpbird 260 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)))
10592, 100oveq12d 7231 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → (((Homf𝐶)‘𝑥)(Hom ‘𝐷)((Homf𝐶)‘𝑦)) = (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)))
106104, 105eleqtrrd 2841 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)) ∈ (((Homf𝐶)‘𝑥)(Hom ‘𝐷)((Homf𝐶)‘𝑦)))
107106ralrimivva 3112 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ∀𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥))∀𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)) ∈ (((Homf𝐶)‘𝑥)(Hom ‘𝐷)((Homf𝐶)‘𝑦)))
108 eqid 2737 . . . . . . 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𝑦))𝑓)))
109108fmpo 7838 . . . . . 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𝐶)‘𝑦)))
110107, 109sylib 221 . . . . 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𝐶)‘𝑦)))
11112oveqd 7230 . . . . . . 7 (𝜑 → (𝑥(2nd𝑀)𝑦) = (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓))))𝑦))
11242ovmpt4g 7356 . . . . . . . 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𝑦))𝑓))))
11345, 112mp3an3 1452 . . . . . . 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𝑦))𝑓))))
114111, 113sylan9eq 2798 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd𝑀)𝑦) = (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓))))
115 eqid 2737 . . . . . . . 8 (Hom ‘𝑂) = (Hom ‘𝑂)
116 simprl 771 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)))
117 simprr 773 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))
11815, 18, 115, 4, 20, 116, 117xpchom 17687 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st𝑥)(Hom ‘𝑂)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
1194, 16oppchom 17219 . . . . . . . 8 ((1st𝑥)(Hom ‘𝑂)(1st𝑦)) = ((1st𝑦)(Hom ‘𝐶)(1st𝑥))
120119xpeq1i 5577 . . . . . . 7 (((1st𝑥)(Hom ‘𝑂)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) = (((1st𝑦)(Hom ‘𝐶)(1st𝑥)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))
121118, 120eqtrdi 2794 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st𝑦)(Hom ‘𝐶)(1st𝑥)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
122114, 121feq12d 6533 . . . . 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𝐶)‘𝑦))))
123110, 122mpbird 260 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)⟶(((Homf𝐶)‘𝑥)(Hom ‘𝐷)((Homf𝐶)‘𝑦)))
124 eqid 2737 . . . . . . . . . 10 (Id‘𝐶) = (Id‘𝐶)
1252ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → 𝐶 ∈ Cat)
12655adantl 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st𝑥) ∈ (Base‘𝐶))
127126adantr 484 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → (1st𝑥) ∈ (Base‘𝐶))
12867adantl 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd𝑥) ∈ (Base‘𝐶))
129128adantr 484 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → (2nd𝑥) ∈ (Base‘𝐶))
130 simpr 488 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
1313, 4, 124, 125, 127, 5, 129, 130catlid 17186 . . . . . . . . 9 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → (((Id‘𝐶)‘(2nd𝑥))(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑥))𝑓) = 𝑓)
132131oveq1d 7228 . . . . . . . 8 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → ((((Id‘𝐶)‘(2nd𝑥))(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑥))𝑓)(⟨(1st𝑥), (1st𝑥)⟩(comp‘𝐶)(2nd𝑥))((Id‘𝐶)‘(1st𝑥))) = (𝑓(⟨(1st𝑥), (1st𝑥)⟩(comp‘𝐶)(2nd𝑥))((Id‘𝐶)‘(1st𝑥))))
1333, 4, 124, 125, 127, 5, 129, 130catrid 17187 . . . . . . . 8 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → (𝑓(⟨(1st𝑥), (1st𝑥)⟩(comp‘𝐶)(2nd𝑥))((Id‘𝐶)‘(1st𝑥))) = 𝑓)
134132, 133eqtrd 2777 . . . . . . 7 (((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) → ((((Id‘𝐶)‘(2nd𝑥))(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑥))𝑓)(⟨(1st𝑥), (1st𝑥)⟩(comp‘𝐶)(2nd𝑥))((Id‘𝐶)‘(1st𝑥))) = 𝑓)
135134mpteq2dva 5150 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)) ↦ ((((Id‘𝐶)‘(2nd𝑥))(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑥))𝑓)(⟨(1st𝑥), (1st𝑥)⟩(comp‘𝐶)(2nd𝑥))((Id‘𝐶)‘(1st𝑥)))) = (𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)) ↦ 𝑓))
136 df-ov 7216 . . . . . . 7 (((Id‘𝐶)‘(1st𝑥))(⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑥), (2nd𝑥)⟩)((Id‘𝐶)‘(2nd𝑥))) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑥), (2nd𝑥)⟩)‘⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐶)‘(2nd𝑥))⟩)
1372adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝐶 ∈ Cat)
1383, 4, 124, 137, 126catidcl 17185 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(1st𝑥)) ∈ ((1st𝑥)(Hom ‘𝐶)(1st𝑥)))
1393, 4, 124, 137, 128catidcl 17185 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(2nd𝑥)) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑥)))
1401, 137, 3, 4, 126, 128, 126, 128, 5, 138, 139hof2val 17764 . . . . . . 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𝑥)))))
141136, 140eqtr3id 2792 . . . . . 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𝑥)))))
14262adantl 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
143142fveq2d 6721 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf𝐶)‘𝑥) = ((Homf𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩))
144143, 90eqtr4di 2796 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf𝐶)‘𝑥) = ((1st𝑥)(Homf𝐶)(2nd𝑥)))
14533, 3, 4, 126, 128homfval 17195 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((1st𝑥)(Homf𝐶)(2nd𝑥)) = ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
146144, 145eqtrd 2777 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf𝐶)‘𝑥) = ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
147146reseq2d 5851 . . . . . . 7 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Homf𝐶)‘𝑥)) = ( I ↾ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))))
148 mptresid 5918 . . . . . . 7 ( I ↾ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))) = (𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)) ↦ 𝑓)
149147, 148eqtrdi 2794 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Homf𝐶)‘𝑥)) = (𝑓 ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)) ↦ 𝑓))
150135, 141, 1493eqtr4d 2787 . . . . 5 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑥), (2nd𝑥)⟩)‘⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐶)‘(2nd𝑥))⟩) = ( I ↾ ((Homf𝐶)‘𝑥)))
151142, 142oveq12d 7231 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(2nd𝑀)𝑥) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑥), (2nd𝑥)⟩))
152142fveq2d 6721 . . . . . . 7 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = ((Id‘(𝑂 ×c 𝐶))‘⟨(1st𝑥), (2nd𝑥)⟩))
15327adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑂 ∈ Cat)
154 eqid 2737 . . . . . . . 8 (Id‘𝑂) = (Id‘𝑂)
15515, 153, 137, 17, 3, 154, 124, 22, 126, 128xpcid 17696 . . . . . . 7 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘⟨(1st𝑥), (2nd𝑥)⟩) = ⟨((Id‘𝑂)‘(1st𝑥)), ((Id‘𝐶)‘(2nd𝑥))⟩)
15616, 124oppcid 17225 . . . . . . . . . 10 (𝐶 ∈ Cat → (Id‘𝑂) = (Id‘𝐶))
157137, 156syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (Id‘𝑂) = (Id‘𝐶))
158157fveq1d 6719 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝑂)‘(1st𝑥)) = ((Id‘𝐶)‘(1st𝑥)))
159158opeq1d 4790 . . . . . . 7 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ⟨((Id‘𝑂)‘(1st𝑥)), ((Id‘𝐶)‘(2nd𝑥))⟩ = ⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐶)‘(2nd𝑥))⟩)
160152, 155, 1593eqtrd 2781 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = ⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐶)‘(2nd𝑥))⟩)
161151, 160fveq12d 6724 . . . . 5 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑥), (2nd𝑥)⟩)‘⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐶)‘(2nd𝑥))⟩))
16229adantr 484 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑈𝑉)
16338ffvelrnda 6904 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf𝐶)‘𝑥) ∈ 𝑈)
16430, 23, 162, 163setcid 17592 . . . . 5 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐷)‘((Homf𝐶)‘𝑥)) = ( I ↾ ((Homf𝐶)‘𝑥)))
165150, 161, 1643eqtr4d 2787 . . . 4 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((Homf𝐶)‘𝑥)))
16623ad2ant1 1135 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat)
167293ad2ant1 1135 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑈𝑉)
168363ad2ant1 1135 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ran (Homf𝐶) ⊆ 𝑈)
169 simp21 1208 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)))
170169, 55syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st𝑥) ∈ (Base‘𝐶))
171169, 67syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd𝑥) ∈ (Base‘𝐶))
172 simp22 1209 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))
173172, 51syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st𝑦) ∈ (Base‘𝐶))
174172, 58syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd𝑦) ∈ (Base‘𝐶))
175 simp23 1210 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)))
176 xp1st 7793 . . . . . . 7 (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st𝑧) ∈ (Base‘𝐶))
177175, 176syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st𝑧) ∈ (Base‘𝐶))
178 xp2nd 7794 . . . . . . 7 (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd𝑧) ∈ (Base‘𝐶))
179175, 178syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd𝑧) ∈ (Base‘𝐶))
180 simp3l 1203 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦))
18115, 18, 115, 4, 20, 169, 172xpchom 17687 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st𝑥)(Hom ‘𝑂)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
182180, 181eleqtrd 2840 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st𝑥)(Hom ‘𝑂)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
183 xp1st 7793 . . . . . . . 8 (𝑓 ∈ (((1st𝑥)(Hom ‘𝑂)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) → (1st𝑓) ∈ ((1st𝑥)(Hom ‘𝑂)(1st𝑦)))
184182, 183syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st𝑓) ∈ ((1st𝑥)(Hom ‘𝑂)(1st𝑦)))
185184, 119eleqtrdi 2848 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st𝑓) ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)))
186 xp2nd 7794 . . . . . . 7 (𝑓 ∈ (((1st𝑥)(Hom ‘𝑂)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) → (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))
187182, 186syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))
188 simp3r 1204 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))
18915, 18, 115, 4, 20, 172, 175xpchom 17687 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧) = (((1st𝑦)(Hom ‘𝑂)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
190188, 189eleqtrd 2840 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st𝑦)(Hom ‘𝑂)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
191 xp1st 7793 . . . . . . . 8 (𝑔 ∈ (((1st𝑦)(Hom ‘𝑂)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) → (1st𝑔) ∈ ((1st𝑦)(Hom ‘𝑂)(1st𝑧)))
192190, 191syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st𝑔) ∈ ((1st𝑦)(Hom ‘𝑂)(1st𝑧)))
1934, 16oppchom 17219 . . . . . . 7 ((1st𝑦)(Hom ‘𝑂)(1st𝑧)) = ((1st𝑧)(Hom ‘𝐶)(1st𝑦))
194192, 193eleqtrdi 2848 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st𝑔) ∈ ((1st𝑧)(Hom ‘𝐶)(1st𝑦)))
195 xp2nd 7794 . . . . . . 7 (𝑔 ∈ (((1st𝑦)(Hom ‘𝑂)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) → (2nd𝑔) ∈ ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧)))
196190, 195syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd𝑔) ∈ ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧)))
1971, 16, 30, 166, 167, 168, 3, 4, 170, 171, 173, 174, 177, 179, 185, 187, 194, 196hofcllem 17766 . . . . 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𝑓))))
198169, 62syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
199 1st2nd2 7800 . . . . . . . . 9 (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
200175, 199syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
201198, 200oveq12d 7231 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd𝑀)𝑧) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑧), (2nd𝑧)⟩))
202172, 79syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
203198, 202opeq12d 4792 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩)
204203, 200oveq12d 7231 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧) = (⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑂 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩))
205 1st2nd2 7800 . . . . . . . . . 10 (𝑔 ∈ (((1st𝑦)(Hom ‘𝑂)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
206190, 205syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
207 1st2nd2 7800 . . . . . . . . . 10 (𝑓 ∈ (((1st𝑥)(Hom ‘𝑂)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
208182, 207syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
209204, 206, 208oveq123d 7234 . . . . . . . 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 2737 . . . . . . . . 9 (comp‘𝑂) = (comp‘𝑂)
21115, 17, 3, 115, 4, 170, 171, 173, 174, 210, 5, 24, 177, 179, 184, 187, 192, 196xpcco2 17694 . . . . . . . 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𝑓))⟩)
2123, 5, 16, 170, 173, 177oppcco 17221 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st𝑔)(⟨(1st𝑥), (1st𝑦)⟩(comp‘𝑂)(1st𝑧))(1st𝑓)) = ((1st𝑓)(⟨(1st𝑧), (1st𝑦)⟩(comp‘𝐶)(1st𝑥))(1st𝑔)))
213212opeq1d 4790 . . . . . . . 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𝑓))⟩)
214209, 211, 2133eqtrd 2781 . . . . . . 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𝑓))⟩)
215201, 214fveq12d 6724 . . . . . 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 7216 . . . . . 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𝑓))⟩)
217215, 216eqtr4di 2796 . . . . 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𝑓))))
218198fveq2d 6721 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑥) = ((Homf𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩))
219218, 90eqtr4di 2796 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑥) = ((1st𝑥)(Homf𝐶)(2nd𝑥)))
22033, 3, 4, 170, 171homfval 17195 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st𝑥)(Homf𝐶)(2nd𝑥)) = ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
221219, 220eqtrd 2777 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑥) = ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
222202fveq2d 6721 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑦) = ((Homf𝐶)‘⟨(1st𝑦), (2nd𝑦)⟩))
223222, 98eqtr4di 2796 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑦) = ((1st𝑦)(Homf𝐶)(2nd𝑦)))
22433, 3, 4, 173, 174homfval 17195 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st𝑦)(Homf𝐶)(2nd𝑦)) = ((1st𝑦)(Hom ‘𝐶)(2nd𝑦)))
225223, 224eqtrd 2777 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑦) = ((1st𝑦)(Hom ‘𝐶)(2nd𝑦)))
226221, 225opeq12d 4792 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ⟨((Homf𝐶)‘𝑥), ((Homf𝐶)‘𝑦)⟩ = ⟨((1st𝑥)(Hom ‘𝐶)(2nd𝑥)), ((1st𝑦)(Hom ‘𝐶)(2nd𝑦))⟩)
227200fveq2d 6721 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑧) = ((Homf𝐶)‘⟨(1st𝑧), (2nd𝑧)⟩))
228 df-ov 7216 . . . . . . . . 9 ((1st𝑧)(Homf𝐶)(2nd𝑧)) = ((Homf𝐶)‘⟨(1st𝑧), (2nd𝑧)⟩)
229227, 228eqtr4di 2796 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑧) = ((1st𝑧)(Homf𝐶)(2nd𝑧)))
23033, 3, 4, 177, 179homfval 17195 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st𝑧)(Homf𝐶)(2nd𝑧)) = ((1st𝑧)(Hom ‘𝐶)(2nd𝑧)))
231229, 230eqtrd 2777 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf𝐶)‘𝑧) = ((1st𝑧)(Hom ‘𝐶)(2nd𝑧)))
232226, 231oveq12d 7231 . . . . . 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𝑧))))
233202, 200oveq12d 7231 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(2nd𝑀)𝑧) = (⟨(1st𝑦), (2nd𝑦)⟩(2nd𝑀)⟨(1st𝑧), (2nd𝑧)⟩))
234233, 206fveq12d 6724 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd𝑀)𝑧)‘𝑔) = ((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝑀)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩))
235 df-ov 7216 . . . . . . 7 ((1st𝑔)(⟨(1st𝑦), (2nd𝑦)⟩(2nd𝑀)⟨(1st𝑧), (2nd𝑧)⟩)(2nd𝑔)) = ((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝑀)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩)
236234, 235eqtr4di 2796 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd𝑀)𝑧)‘𝑔) = ((1st𝑔)(⟨(1st𝑦), (2nd𝑦)⟩(2nd𝑀)⟨(1st𝑧), (2nd𝑧)⟩)(2nd𝑔)))
237198, 202oveq12d 7231 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd𝑀)𝑦) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑦), (2nd𝑦)⟩))
238237, 208fveq12d 6724 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd𝑀)𝑦)‘𝑓) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩))
239 df-ov 7216 . . . . . . 7 ((1st𝑓)(⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑦), (2nd𝑦)⟩)(2nd𝑓)) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩)
240238, 239eqtr4di 2796 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd𝑀)𝑦)‘𝑓) = ((1st𝑓)(⟨(1st𝑥), (2nd𝑥)⟩(2nd𝑀)⟨(1st𝑦), (2nd𝑦)⟩)(2nd𝑓)))
241232, 236, 240oveq123d 7234 . . . . 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𝑓))))
242197, 217, 2413eqtr4d 2787 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd𝑀)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = (((𝑦(2nd𝑀)𝑧)‘𝑔)(⟨((Homf𝐶)‘𝑥), ((Homf𝐶)‘𝑦)⟩(comp‘𝐷)((Homf𝐶)‘𝑧))((𝑥(2nd𝑀)𝑦)‘𝑓)))
24318, 19, 20, 21, 22, 23, 24, 25, 28, 32, 41, 48, 123, 165, 242isfuncd 17371 . . 3 (𝜑 → (Homf𝐶)((𝑂 ×c 𝐶) Func 𝐷)(2nd𝑀))
244 df-br 5054 . . 3 ((Homf𝐶)((𝑂 ×c 𝐶) Func 𝐷)(2nd𝑀) ↔ ⟨(Homf𝐶), (2nd𝑀)⟩ ∈ ((𝑂 ×c 𝐶) Func 𝐷))
245243, 244sylib 221 . 2 (𝜑 → ⟨(Homf𝐶), (2nd𝑀)⟩ ∈ ((𝑂 ×c 𝐶) Func 𝐷))
24614, 245eqeltrd 2838 1 (𝜑𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2110  wral 3061  Vcvv 3408  wss 3866  cop 4547   class class class wbr 5053  cmpt 5135   I cid 5454   × cxp 5549  ran crn 5552  cres 5553   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  cmpo 7215  1st c1st 7759  2nd c2nd 7760  Basecbs 16760  Hom chom 16813  compcco 16814  Catccat 17167  Idccid 17168  Homf chomf 17169  oppCatcoppc 17214   Func cfunc 17360  SetCatcsetc 17581   ×c cxpc 17675  HomFchof 17756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-tpos 7968  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-map 8510  df-ixp 8579  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-z 12177  df-dec 12294  df-uz 12439  df-fz 13096  df-struct 16700  df-sets 16717  df-slot 16735  df-ndx 16745  df-base 16761  df-hom 16826  df-cco 16827  df-cat 17171  df-cid 17172  df-homf 17173  df-oppc 17215  df-func 17364  df-setc 17582  df-xpc 17679  df-hof 17758
This theorem is referenced by:  oppchofcl  17768  oppcyon  17777  yonedalem1  17780  yonedalem21  17781  yonedalem22  17786
  Copyright terms: Public domain W3C validator