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

Theorem funcpropd 17165
 Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.)
Hypotheses
Ref Expression
funcpropd.1 (𝜑 → (Homf𝐴) = (Homf𝐵))
funcpropd.2 (𝜑 → (compf𝐴) = (compf𝐵))
funcpropd.3 (𝜑 → (Homf𝐶) = (Homf𝐷))
funcpropd.4 (𝜑 → (compf𝐶) = (compf𝐷))
funcpropd.a (𝜑𝐴𝑉)
funcpropd.b (𝜑𝐵𝑉)
funcpropd.c (𝜑𝐶𝑉)
funcpropd.d (𝜑𝐷𝑉)
Assertion
Ref Expression
funcpropd (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))

Proof of Theorem funcpropd
Dummy variables 𝑓 𝑔 𝑚 𝑛 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 17127 . 2 Rel (𝐴 Func 𝐶)
2 relfunc 17127 . 2 Rel (𝐵 Func 𝐷)
3 funcpropd.1 . . . . . 6 (𝜑 → (Homf𝐴) = (Homf𝐵))
4 funcpropd.2 . . . . . 6 (𝜑 → (compf𝐴) = (compf𝐵))
5 funcpropd.a . . . . . 6 (𝜑𝐴𝑉)
6 funcpropd.b . . . . . 6 (𝜑𝐵𝑉)
73, 4, 5, 6catpropd 16974 . . . . 5 (𝜑 → (𝐴 ∈ Cat ↔ 𝐵 ∈ Cat))
8 funcpropd.3 . . . . . 6 (𝜑 → (Homf𝐶) = (Homf𝐷))
9 funcpropd.4 . . . . . 6 (𝜑 → (compf𝐶) = (compf𝐷))
10 funcpropd.c . . . . . 6 (𝜑𝐶𝑉)
11 funcpropd.d . . . . . 6 (𝜑𝐷𝑉)
128, 9, 10, 11catpropd 16974 . . . . 5 (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
137, 12anbi12d 633 . . . 4 (𝜑 → ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ↔ (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat)))
14 2fveq3 6654 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (𝑓‘(1st𝑧)) = (𝑓‘(1st𝑤)))
15 2fveq3 6654 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (𝑓‘(2nd𝑧)) = (𝑓‘(2nd𝑤)))
1614, 15oveq12d 7157 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) = ((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))))
17 fveq2 6649 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘𝑤))
1816, 17oveq12d 7157 . . . . . . . . . . 11 (𝑧 = 𝑤 → (((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))
1918cbvixpv 8466 . . . . . . . . . 10 X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) = X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤))
2019eleq2i 2884 . . . . . . . . 9 (𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))
2120anbi2i 625 . . . . . . . 8 ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤))))
223ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Homf𝐴) = (Homf𝐵))
234ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (compf𝐴) = (compf𝐵))
245ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐴𝑉)
256ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐵𝑉)
2622, 23, 24, 25cidpropd 16975 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐴) = (Id‘𝐵))
2726fveq1d 6651 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐴)‘𝑥) = ((Id‘𝐵)‘𝑥))
2827fveq2d 6653 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)))
298, 9, 10, 11cidpropd 16975 . . . . . . . . . . . . 13 (𝜑 → (Id‘𝐶) = (Id‘𝐷))
3029ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐶) = (Id‘𝐷))
3130fveq1d 6651 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐶)‘(𝑓𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)))
3228, 31eqeq12d 2817 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ↔ ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥))))
33 eqid 2801 . . . . . . . . . . . . . . . . . 18 (Base‘𝐴) = (Base‘𝐴)
34 eqid 2801 . . . . . . . . . . . . . . . . . 18 (Hom ‘𝐴) = (Hom ‘𝐴)
35 eqid 2801 . . . . . . . . . . . . . . . . . 18 (comp‘𝐴) = (comp‘𝐴)
36 eqid 2801 . . . . . . . . . . . . . . . . . 18 (comp‘𝐵) = (comp‘𝐵)
373ad6antr 735 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf𝐴) = (Homf𝐵))
384ad6antr 735 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (compf𝐴) = (compf𝐵))
39 simp-5r 785 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑥 ∈ (Base‘𝐴))
40 simp-4r 783 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑦 ∈ (Base‘𝐴))
41 simpllr 775 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑧 ∈ (Base‘𝐴))
42 simplr 768 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦))
43 simpr 488 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧))
4433, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43comfeqval 16973 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚))
4544fveq2d 6653 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)))
46 eqid 2801 . . . . . . . . . . . . . . . . 17 (Base‘𝐶) = (Base‘𝐶)
47 eqid 2801 . . . . . . . . . . . . . . . . 17 (Hom ‘𝐶) = (Hom ‘𝐶)
48 eqid 2801 . . . . . . . . . . . . . . . . 17 (comp‘𝐶) = (comp‘𝐶)
49 eqid 2801 . . . . . . . . . . . . . . . . 17 (comp‘𝐷) = (comp‘𝐷)
508ad6antr 735 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf𝐶) = (Homf𝐷))
519ad6antr 735 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (compf𝐶) = (compf𝐷))
52 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
5352ad5antr 733 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
5453, 39ffvelrnd 6833 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓𝑥) ∈ (Base‘𝐶))
5553, 40ffvelrnd 6833 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓𝑦) ∈ (Base‘𝐶))
5653, 41ffvelrnd 6833 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓𝑧) ∈ (Base‘𝐶))
57 df-ov 7142 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑔𝑦) = (𝑔‘⟨𝑥, 𝑦⟩)
58 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) → 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))
5958ad5ant12 755 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))
6059adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))
61 opelxpi 5560 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
6261ad5ant23 759 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
63 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
64 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑦 ∈ V
6563, 64op1std 7685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑥, 𝑦⟩ → (1st𝑤) = 𝑥)
6665fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(1st𝑤)) = (𝑓𝑥))
6763, 64op2ndd 7686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑥, 𝑦⟩ → (2nd𝑤) = 𝑦)
6867fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(2nd𝑤)) = (𝑓𝑦))
6966, 68oveq12d 7157 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) = ((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
70 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩))
71 df-ov 7142 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥(Hom ‘𝐴)𝑦) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩)
7270, 71eqtr4di 2854 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑥(Hom ‘𝐴)𝑦))
7369, 72oveq12d 7157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ⟨𝑥, 𝑦⟩ → (((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)) = (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦)))
7473fvixp 8453 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦)))
7560, 62, 74syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦)))
7657, 75eqeltrid 2897 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦)))
77 elmapi 8415 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑔𝑦) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
7876, 77syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
7978adantr 484 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
8079, 42ffvelrnd 6833 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑦)‘𝑚) ∈ ((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
81 df-ov 7142 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑔𝑧) = (𝑔‘⟨𝑦, 𝑧⟩)
82 opelxpi 5560 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ (Base‘𝐴) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
8382adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
84 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 ∈ V
8564, 84op1std 7685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑦, 𝑧⟩ → (1st𝑤) = 𝑦)
8685fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(1st𝑤)) = (𝑓𝑦))
8764, 84op2ndd 7686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑦, 𝑧⟩ → (2nd𝑤) = 𝑧)
8887fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(2nd𝑤)) = (𝑓𝑧))
8986, 88oveq12d 7157 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) = ((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
90 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩))
91 df-ov 7142 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦(Hom ‘𝐴)𝑧) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩)
9290, 91eqtr4di 2854 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑦(Hom ‘𝐴)𝑧))
9389, 92oveq12d 7157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ⟨𝑦, 𝑧⟩ → (((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)) = (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧)))
9493fvixp 8453 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧)))
9559, 83, 94syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧)))
9681, 95eqeltrid 2897 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧)))
97 elmapi 8415 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑔𝑧) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
9896, 97syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
9998adantr 484 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
10099ffvelrnda 6832 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑦𝑔𝑧)‘𝑛) ∈ ((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
10146, 47, 48, 49, 50, 51, 54, 55, 56, 80, 100comfeqval 16973 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))
10245, 101eqeq12d 2817 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
103102ralbidva 3164 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
104103ralbidva 3164 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
105 eqid 2801 . . . . . . . . . . . . . . 15 (Hom ‘𝐵) = (Hom ‘𝐵)
10622ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Homf𝐴) = (Homf𝐵))
107 simpllr 775 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑥 ∈ (Base‘𝐴))
108 simplr 768 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑦 ∈ (Base‘𝐴))
10933, 34, 105, 106, 107, 108homfeqval 16962 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑥(Hom ‘𝐴)𝑦) = (𝑥(Hom ‘𝐵)𝑦))
110 simpr 488 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
11133, 34, 105, 106, 108, 110homfeqval 16962 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦(Hom ‘𝐴)𝑧) = (𝑦(Hom ‘𝐵)𝑧))
112111raleqdv 3367 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
113109, 112raleqbidv 3357 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
114104, 113bitrd 282 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
115114ralbidva 3164 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
116115ralbidva 3164 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
11732, 116anbi12d 633 . . . . . . . . 9 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
118117ralbidva 3164 . . . . . . . 8 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑m ((Hom ‘𝐴)‘𝑤)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
11921, 118sylan2b 596 . . . . . . 7 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
120119pm5.32da 582 . . . . . 6 (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
121 eqid 2801 . . . . . . . . . . . . . 14 (Hom ‘𝐷) = (Hom ‘𝐷)
1228ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf𝐶) = (Homf𝐷))
123 simplr 768 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
124 xp1st 7707 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (1st𝑧) ∈ (Base‘𝐴))
125124adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (1st𝑧) ∈ (Base‘𝐴))
126123, 125ffvelrnd 6833 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(1st𝑧)) ∈ (Base‘𝐶))
127 xp2nd 7708 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (2nd𝑧) ∈ (Base‘𝐴))
128127adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (2nd𝑧) ∈ (Base‘𝐴))
129123, 128ffvelrnd 6833 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(2nd𝑧)) ∈ (Base‘𝐶))
13046, 47, 121, 122, 126, 129homfeqval 16962 . . . . . . . . . . . . 13 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) = ((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))))
1313ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf𝐴) = (Homf𝐵))
13233, 34, 105, 131, 125, 128homfeqval 16962 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((1st𝑧)(Hom ‘𝐴)(2nd𝑧)) = ((1st𝑧)(Hom ‘𝐵)(2nd𝑧)))
133 df-ov 7142 . . . . . . . . . . . . . . 15 ((1st𝑧)(Hom ‘𝐴)(2nd𝑧)) = ((Hom ‘𝐴)‘⟨(1st𝑧), (2nd𝑧)⟩)
134 df-ov 7142 . . . . . . . . . . . . . . 15 ((1st𝑧)(Hom ‘𝐵)(2nd𝑧)) = ((Hom ‘𝐵)‘⟨(1st𝑧), (2nd𝑧)⟩)
135132, 133, 1343eqtr3g 2859 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘⟨(1st𝑧), (2nd𝑧)⟩) = ((Hom ‘𝐵)‘⟨(1st𝑧), (2nd𝑧)⟩))
136 1st2nd2 7714 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
137136adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
138137fveq2d 6653 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘⟨(1st𝑧), (2nd𝑧)⟩))
139137fveq2d 6653 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐵)‘𝑧) = ((Hom ‘𝐵)‘⟨(1st𝑧), (2nd𝑧)⟩))
140135, 138, 1393eqtr4d 2846 . . . . . . . . . . . . 13 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐵)‘𝑧))
141130, 140oveq12d 7157 . . . . . . . . . . . 12 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)))
142141ixpeq2dva 8463 . . . . . . . . . . 11 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)))
1433homfeqbas 16961 . . . . . . . . . . . . . 14 (𝜑 → (Base‘𝐴) = (Base‘𝐵))
144143sqxpeqd 5555 . . . . . . . . . . . . 13 (𝜑 → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
145144adantr 484 . . . . . . . . . . . 12 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
146145ixpeq1d 8460 . . . . . . . . . . 11 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)))
147142, 146eqtrd 2836 . . . . . . . . . 10 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)))
148147eleq2d 2878 . . . . . . . . 9 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → (𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧))))
149148pm5.32da 582 . . . . . . . 8 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)))))
1508homfeqbas 16961 . . . . . . . . . 10 (𝜑 → (Base‘𝐶) = (Base‘𝐷))
151143, 150feq23d 6486 . . . . . . . . 9 (𝜑 → (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ↔ 𝑓:(Base‘𝐵)⟶(Base‘𝐷)))
152151anbi1d 632 . . . . . . . 8 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)))))
153149, 152bitrd 282 . . . . . . 7 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)))))
154143adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
155154raleqdv 3367 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
156154, 155raleqbidv 3357 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
157156anbi2d 631 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
158143, 157raleqbidva 3373 . . . . . . 7 (𝜑 → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
159153, 158anbi12d 633 . . . . . 6 (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
160120, 159bitrd 282 . . . . 5 (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
161 df-3an 1086 . . . . 5 ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
162 df-3an 1086 . . . . 5 ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
163160, 161, 1623bitr4g 317 . . . 4 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
16413, 163anbi12d 633 . . 3 (𝜑 → (((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))) ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))))
165 df-br 5034 . . . . 5 (𝑓(𝐴 Func 𝐶)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶))
166 funcrcl 17128 . . . . 5 (⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶) → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
167165, 166sylbi 220 . . . 4 (𝑓(𝐴 Func 𝐶)𝑔 → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
168 eqid 2801 . . . . 5 (Id‘𝐴) = (Id‘𝐴)
169 eqid 2801 . . . . 5 (Id‘𝐶) = (Id‘𝐶)
170 simpl 486 . . . . 5 ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐴 ∈ Cat)
171 simpr 488 . . . . 5 ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat)
17233, 46, 34, 47, 168, 169, 35, 48, 170, 171isfunc 17129 . . . 4 ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → (𝑓(𝐴 Func 𝐶)𝑔 ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
173167, 172biadanii 821 . . 3 (𝑓(𝐴 Func 𝐶)𝑔 ↔ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
174 df-br 5034 . . . . 5 (𝑓(𝐵 Func 𝐷)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷))
175 funcrcl 17128 . . . . 5 (⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷) → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
176174, 175sylbi 220 . . . 4 (𝑓(𝐵 Func 𝐷)𝑔 → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
177 eqid 2801 . . . . 5 (Base‘𝐵) = (Base‘𝐵)
178 eqid 2801 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
179 eqid 2801 . . . . 5 (Id‘𝐵) = (Id‘𝐵)
180 eqid 2801 . . . . 5 (Id‘𝐷) = (Id‘𝐷)
181 simpl 486 . . . . 5 ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐵 ∈ Cat)
182 simpr 488 . . . . 5 ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐷 ∈ Cat)
183177, 178, 105, 121, 179, 180, 36, 49, 181, 182isfunc 17129 . . . 4 ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓(𝐵 Func 𝐷)𝑔 ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
184176, 183biadanii 821 . . 3 (𝑓(𝐵 Func 𝐷)𝑔 ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
185164, 173, 1843bitr4g 317 . 2 (𝜑 → (𝑓(𝐴 Func 𝐶)𝑔𝑓(𝐵 Func 𝐷)𝑔))
1861, 2, 185eqbrrdiv 5635 1 (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  ∀wral 3109  ⟨cop 4534   class class class wbr 5033   × cxp 5521  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139  1st c1st 7673  2nd c2nd 7674   ↑m cmap 8393  Xcixp 8448  Basecbs 16478  Hom chom 16571  compcco 16572  Catccat 16930  Idccid 16931  Homf chomf 16932  compfccomf 16933   Func cfunc 17119 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-1st 7675  df-2nd 7676  df-map 8395  df-ixp 8449  df-cat 16934  df-cid 16935  df-homf 16936  df-comf 16937  df-func 17123 This theorem is referenced by:  funcres2c  17166  fullpropd  17185  fthpropd  17186  ressffth  17203  natpropd  17241  fucpropd  17242  funcsetcres2  17348
 Copyright terms: Public domain W3C validator