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

Theorem hofpropd 17517
Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
Hypotheses
Ref Expression
hofpropd.1 (𝜑 → (Homf𝐶) = (Homf𝐷))
hofpropd.2 (𝜑 → (compf𝐶) = (compf𝐷))
hofpropd.c (𝜑𝐶 ∈ Cat)
hofpropd.d (𝜑𝐷 ∈ Cat)
Assertion
Ref Expression
hofpropd (𝜑 → (HomF𝐶) = (HomF𝐷))

Proof of Theorem hofpropd
Dummy variables 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofpropd.1 . . 3 (𝜑 → (Homf𝐶) = (Homf𝐷))
21homfeqbas 16966 . . . . 5 (𝜑 → (Base‘𝐶) = (Base‘𝐷))
32sqxpeqd 5574 . . . 4 (𝜑 → ((Base‘𝐶) × (Base‘𝐶)) = ((Base‘𝐷) × (Base‘𝐷)))
43adantr 484 . . . 4 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Base‘𝐶) × (Base‘𝐶)) = ((Base‘𝐷) × (Base‘𝐷)))
5 eqid 2824 . . . . . 6 (Base‘𝐶) = (Base‘𝐶)
6 eqid 2824 . . . . . 6 (Hom ‘𝐶) = (Hom ‘𝐶)
7 eqid 2824 . . . . . 6 (Hom ‘𝐷) = (Hom ‘𝐷)
81adantr 484 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (Homf𝐶) = (Homf𝐷))
9 xp1st 7716 . . . . . . 7 (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st𝑦) ∈ (Base‘𝐶))
109ad2antll 728 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (1st𝑦) ∈ (Base‘𝐶))
11 xp1st 7716 . . . . . . 7 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st𝑥) ∈ (Base‘𝐶))
1211ad2antrl 727 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (1st𝑥) ∈ (Base‘𝐶))
135, 6, 7, 8, 10, 12homfeqval 16967 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) = ((1st𝑦)(Hom ‘𝐷)(1st𝑥)))
14 xp2nd 7717 . . . . . . . 8 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd𝑥) ∈ (Base‘𝐶))
1514ad2antrl 727 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (2nd𝑥) ∈ (Base‘𝐶))
16 xp2nd 7717 . . . . . . . 8 (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd𝑦) ∈ (Base‘𝐶))
1716ad2antll 728 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (2nd𝑦) ∈ (Base‘𝐶))
185, 6, 7, 8, 15, 17homfeqval 16967 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) = ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))
1918adantr 484 . . . . 5 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ 𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥))) → ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) = ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))
205, 6, 7, 8, 12, 15homfeqval 16967 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)) = ((1st𝑥)(Hom ‘𝐷)(2nd𝑥)))
21 df-ov 7152 . . . . . . . . 9 ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)) = ((Hom ‘𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩)
22 df-ov 7152 . . . . . . . . 9 ((1st𝑥)(Hom ‘𝐷)(2nd𝑥)) = ((Hom ‘𝐷)‘⟨(1st𝑥), (2nd𝑥)⟩)
2320, 21, 223eqtr3g 2882 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩) = ((Hom ‘𝐷)‘⟨(1st𝑥), (2nd𝑥)⟩))
24 1st2nd2 7723 . . . . . . . . . 10 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2524ad2antrl 727 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2625fveq2d 6665 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩))
2725fveq2d 6665 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐷)‘𝑥) = ((Hom ‘𝐷)‘⟨(1st𝑥), (2nd𝑥)⟩))
2823, 26, 273eqtr4d 2869 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐷)‘𝑥))
2928adantr 484 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐷)‘𝑥))
30 eqid 2824 . . . . . . . 8 (comp‘𝐶) = (comp‘𝐶)
31 eqid 2824 . . . . . . . 8 (comp‘𝐷) = (comp‘𝐷)
328ad2antrr 725 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (Homf𝐶) = (Homf𝐷))
33 hofpropd.2 . . . . . . . . 9 (𝜑 → (compf𝐶) = (compf𝐷))
3433ad3antrrr 729 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (compf𝐶) = (compf𝐷))
3510ad2antrr 725 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st𝑦) ∈ (Base‘𝐶))
3612ad2antrr 725 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st𝑥) ∈ (Base‘𝐶))
3717ad2antrr 725 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd𝑦) ∈ (Base‘𝐶))
38 simplrl 776 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)))
3925ad2antrr 725 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
4039oveq1d 7164 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2nd𝑦)) = (⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑦)))
4140oveqd 7166 . . . . . . . . 9 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd𝑦))) = (𝑔(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑦))))
42 hofpropd.c . . . . . . . . . . 11 (𝜑𝐶 ∈ Cat)
4342ad3antrrr 729 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat)
4415ad2antrr 725 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd𝑥) ∈ (Base‘𝐶))
4526adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1st𝑥), (2nd𝑥)⟩))
4645, 21syl6eqr 2877 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
4746eleq2d 2901 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ( ∈ ((Hom ‘𝐶)‘𝑥) ↔ ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥))))
4847biimpa 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑥)))
49 simplrr 777 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))
505, 6, 30, 43, 36, 44, 37, 48, 49catcocl 16956 . . . . . . . . 9 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑦))) ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑦)))
5141, 50eqeltrd 2916 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd𝑦))) ∈ ((1st𝑥)(Hom ‘𝐶)(2nd𝑦)))
525, 6, 30, 31, 32, 34, 35, 36, 37, 38, 51comfeqval 16978 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐷)(2nd𝑦))𝑓))
535, 6, 30, 31, 32, 34, 36, 44, 37, 48, 49comfeqval 16978 . . . . . . . . 9 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐶)(2nd𝑦))) = (𝑔(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐷)(2nd𝑦))))
5439oveq1d 7164 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐷)(2nd𝑦)) = (⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐷)(2nd𝑦)))
5554oveqd 7166 . . . . . . . . 9 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐷)(2nd𝑦))) = (𝑔(⟨(1st𝑥), (2nd𝑥)⟩(comp‘𝐷)(2nd𝑦))))
5653, 41, 553eqtr4d 2869 . . . . . . . 8 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd𝑦))) = (𝑔(𝑥(comp‘𝐷)(2nd𝑦))))
5756oveq1d 7164 . . . . . . 7 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐷)(2nd𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐷)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐷)(2nd𝑦))𝑓))
5852, 57eqtrd 2859 . . . . . 6 ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) ∧ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐷)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐷)(2nd𝑦))𝑓))
5929, 58mpteq12dva 5136 . . . . 5 (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)) ∧ 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)))) → ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓)) = ( ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐷)(2nd𝑦))𝑓)))
6013, 19, 59mpoeq123dva 7221 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((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𝑦))𝑓))))
613, 4, 60mpoeq123dva 7221 . . 3 (𝜑 → (𝑥 ∈ ((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𝑦))𝑓)))))
621, 61opeq12d 4797 . 2 (𝜑 → ⟨(Homf𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓))))⟩ = ⟨(Homf𝐷), (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐷)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐷)(2nd𝑦))𝑓))))⟩)
63 eqid 2824 . . 3 (HomF𝐶) = (HomF𝐶)
6463, 42, 5, 6, 30hofval 17502 . 2 (𝜑 → (HomF𝐶) = ⟨(Homf𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐶)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐶)(2nd𝑦))𝑓))))⟩)
65 eqid 2824 . . 3 (HomF𝐷) = (HomF𝐷)
66 hofpropd.d . . 3 (𝜑𝐷 ∈ Cat)
67 eqid 2824 . . 3 (Base‘𝐷) = (Base‘𝐷)
6865, 66, 67, 7, 31hofval 17502 . 2 (𝜑 → (HomF𝐷) = ⟨(Homf𝐷), (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝐷)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝐷)(2nd𝑦))𝑓))))⟩)
6962, 64, 683eqtr4d 2869 1 (𝜑 → (HomF𝐶) = (HomF𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2115  cop 4556  cmpt 5132   × cxp 5540  cfv 6343  (class class class)co 7149  cmpo 7151  1st c1st 7682  2nd c2nd 7683  Basecbs 16483  Hom chom 16576  compcco 16577  Catccat 16935  Homf chomf 16937  compfccomf 16938  HomFchof 17498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-1st 7684  df-2nd 7685  df-cat 16939  df-homf 16941  df-comf 16942  df-hof 17500
This theorem is referenced by:  yonpropd  17518  oppcyon  17519
  Copyright terms: Public domain W3C validator