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

Theorem funcpropd 16383
 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 16345 . 2 Rel (𝐴 Func 𝐶)
2 relfunc 16345 . 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 16192 . . . . 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 16192 . . . . 5 (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
137, 12anbi12d 743 . . . 4 (𝜑 → ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ↔ (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat)))
14 fveq2 6103 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (1st𝑧) = (1st𝑤))
1514fveq2d 6107 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (𝑓‘(1st𝑧)) = (𝑓‘(1st𝑤)))
16 fveq2 6103 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (2nd𝑧) = (2nd𝑤))
1716fveq2d 6107 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (𝑓‘(2nd𝑧)) = (𝑓‘(2nd𝑤)))
1815, 17oveq12d 6567 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) = ((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))))
19 fveq2 6103 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘𝑤))
2018, 19oveq12d 6567 . . . . . . . . . . 11 (𝑧 = 𝑤 → (((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
2120cbvixpv 7812 . . . . . . . . . 10 X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤))
2221eleq2i 2680 . . . . . . . . 9 (𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
2322anbi2i 726 . . . . . . . 8 ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤))))
243ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Homf𝐴) = (Homf𝐵))
254ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (compf𝐴) = (compf𝐵))
265ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐴𝑉)
276ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐵𝑉)
2824, 25, 26, 27cidpropd 16193 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐴) = (Id‘𝐵))
2928fveq1d 6105 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐴)‘𝑥) = ((Id‘𝐵)‘𝑥))
3029fveq2d 6107 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)))
318, 9, 10, 11cidpropd 16193 . . . . . . . . . . . . 13 (𝜑 → (Id‘𝐶) = (Id‘𝐷))
3231ad2antrr 758 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐶) = (Id‘𝐷))
3332fveq1d 6105 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐶)‘(𝑓𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)))
3430, 33eqeq12d 2625 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ↔ ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥))))
35 eqid 2610 . . . . . . . . . . . . . . . . . 18 (Base‘𝐴) = (Base‘𝐴)
36 eqid 2610 . . . . . . . . . . . . . . . . . 18 (Hom ‘𝐴) = (Hom ‘𝐴)
37 eqid 2610 . . . . . . . . . . . . . . . . . 18 (comp‘𝐴) = (comp‘𝐴)
38 eqid 2610 . . . . . . . . . . . . . . . . . 18 (comp‘𝐵) = (comp‘𝐵)
393ad6antr 768 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf𝐴) = (Homf𝐵))
404ad6antr 768 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (compf𝐴) = (compf𝐵))
41 simp-5r 805 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑥 ∈ (Base‘𝐴))
42 simp-4r 803 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑦 ∈ (Base‘𝐴))
43 simpllr 795 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑧 ∈ (Base‘𝐴))
44 simplr 788 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦))
45 simpr 476 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧))
4635, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45comfeqval 16191 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚))
4746fveq2d 6107 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)))
48 eqid 2610 . . . . . . . . . . . . . . . . 17 (Base‘𝐶) = (Base‘𝐶)
49 eqid 2610 . . . . . . . . . . . . . . . . 17 (Hom ‘𝐶) = (Hom ‘𝐶)
50 eqid 2610 . . . . . . . . . . . . . . . . 17 (comp‘𝐶) = (comp‘𝐶)
51 eqid 2610 . . . . . . . . . . . . . . . . 17 (comp‘𝐷) = (comp‘𝐷)
528ad6antr 768 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf𝐶) = (Homf𝐷))
539ad6antr 768 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (compf𝐶) = (compf𝐷))
54 simprl 790 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
5554ad5antr 766 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
5655, 41ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓𝑥) ∈ (Base‘𝐶))
5755, 42ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓𝑦) ∈ (Base‘𝐶))
5855, 43ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓𝑧) ∈ (Base‘𝐶))
59 df-ov 6552 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑔𝑦) = (𝑔‘⟨𝑥, 𝑦⟩)
60 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) → 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
6160ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
6261adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
63 simp-4r 803 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑥 ∈ (Base‘𝐴))
64 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑦 ∈ (Base‘𝐴))
65 opelxpi 5072 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
6663, 64, 65syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
67 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
68 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑦 ∈ V
6967, 68op1std 7069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑥, 𝑦⟩ → (1st𝑤) = 𝑥)
7069fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(1st𝑤)) = (𝑓𝑥))
7167, 68op2ndd 7070 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑥, 𝑦⟩ → (2nd𝑤) = 𝑦)
7271fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(2nd𝑤)) = (𝑓𝑦))
7370, 72oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) = ((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
74 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩))
75 df-ov 6552 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥(Hom ‘𝐴)𝑦) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩)
7674, 75syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑥(Hom ‘𝐴)𝑦))
7773, 76oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ⟨𝑥, 𝑦⟩ → (((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) = (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
7877fvixp 7799 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
7962, 66, 78syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
8059, 79syl5eqel 2692 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
81 elmapi 7765 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑔𝑦) ∈ (((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
8280, 81syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
8382adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
8483, 44ffvelrnd 6268 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑦)‘𝑚) ∈ ((𝑓𝑥)(Hom ‘𝐶)(𝑓𝑦)))
85 df-ov 6552 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑔𝑧) = (𝑔‘⟨𝑦, 𝑧⟩)
86 opelxpi 5072 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ (Base‘𝐴) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
8786adantll 746 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
88 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 ∈ V
8968, 88op1std 7069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑦, 𝑧⟩ → (1st𝑤) = 𝑦)
9089fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(1st𝑤)) = (𝑓𝑦))
9168, 88op2ndd 7070 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = ⟨𝑦, 𝑧⟩ → (2nd𝑤) = 𝑧)
9291fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(2nd𝑤)) = (𝑓𝑧))
9390, 92oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) = ((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
94 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩))
95 df-ov 6552 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦(Hom ‘𝐴)𝑧) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩)
9694, 95syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑦(Hom ‘𝐴)𝑧))
9793, 96oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = ⟨𝑦, 𝑧⟩ → (((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) = (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
9897fvixp 7799 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
9961, 87, 98syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
10085, 99syl5eqel 2692 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
101 elmapi 7765 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑔𝑧) ∈ (((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
102100, 101syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
103102adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
104103ffvelrnda 6267 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑦𝑔𝑧)‘𝑛) ∈ ((𝑓𝑦)(Hom ‘𝐶)(𝑓𝑧)))
10548, 49, 50, 51, 52, 53, 56, 57, 58, 84, 104comfeqval 16191 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))
10647, 105eqeq12d 2625 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
107106ralbidva 2968 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
108107ralbidva 2968 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
109 eqid 2610 . . . . . . . . . . . . . . 15 (Hom ‘𝐵) = (Hom ‘𝐵)
11024ad2antrr 758 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Homf𝐴) = (Homf𝐵))
111 simpllr 795 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑥 ∈ (Base‘𝐴))
112 simplr 788 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑦 ∈ (Base‘𝐴))
11335, 36, 109, 110, 111, 112homfeqval 16180 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑥(Hom ‘𝐴)𝑦) = (𝑥(Hom ‘𝐵)𝑦))
114 simpr 476 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
11535, 36, 109, 110, 112, 114homfeqval 16180 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦(Hom ‘𝐴)𝑧) = (𝑦(Hom ‘𝐵)𝑧))
116115raleqdv 3121 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
117113, 116raleqbidv 3129 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
118108, 117bitrd 267 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
119118ralbidva 2968 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
120119ralbidva 2968 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
12134, 120anbi12d 743 . . . . . . . . 9 (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
122121ralbidva 2968 . . . . . . . 8 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑤))(Hom ‘𝐶)(𝑓‘(2nd𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
12323, 122sylan2b 491 . . . . . . 7 ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
124123pm5.32da 671 . . . . . 6 (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
125 eqid 2610 . . . . . . . . . . . . . 14 (Hom ‘𝐷) = (Hom ‘𝐷)
1268ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf𝐶) = (Homf𝐷))
127 simplr 788 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
128 xp1st 7089 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (1st𝑧) ∈ (Base‘𝐴))
129128adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (1st𝑧) ∈ (Base‘𝐴))
130127, 129ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(1st𝑧)) ∈ (Base‘𝐶))
131 xp2nd 7090 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (2nd𝑧) ∈ (Base‘𝐴))
132131adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (2nd𝑧) ∈ (Base‘𝐴))
133127, 132ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(2nd𝑧)) ∈ (Base‘𝐶))
13448, 49, 125, 126, 130, 133homfeqval 16180 . . . . . . . . . . . . 13 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) = ((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))))
1353ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf𝐴) = (Homf𝐵))
13635, 36, 109, 135, 129, 132homfeqval 16180 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((1st𝑧)(Hom ‘𝐴)(2nd𝑧)) = ((1st𝑧)(Hom ‘𝐵)(2nd𝑧)))
137 df-ov 6552 . . . . . . . . . . . . . . 15 ((1st𝑧)(Hom ‘𝐴)(2nd𝑧)) = ((Hom ‘𝐴)‘⟨(1st𝑧), (2nd𝑧)⟩)
138 df-ov 6552 . . . . . . . . . . . . . . 15 ((1st𝑧)(Hom ‘𝐵)(2nd𝑧)) = ((Hom ‘𝐵)‘⟨(1st𝑧), (2nd𝑧)⟩)
139136, 137, 1383eqtr3g 2667 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘⟨(1st𝑧), (2nd𝑧)⟩) = ((Hom ‘𝐵)‘⟨(1st𝑧), (2nd𝑧)⟩))
140 1st2nd2 7096 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
141140adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
142141fveq2d 6107 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘⟨(1st𝑧), (2nd𝑧)⟩))
143141fveq2d 6107 . . . . . . . . . . . . . 14 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐵)‘𝑧) = ((Hom ‘𝐵)‘⟨(1st𝑧), (2nd𝑧)⟩))
144139, 142, 1433eqtr4d 2654 . . . . . . . . . . . . 13 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐵)‘𝑧))
145134, 144oveq12d 6567 . . . . . . . . . . . 12 (((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
146145ixpeq2dva 7809 . . . . . . . . . . 11 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
1473homfeqbas 16179 . . . . . . . . . . . . . 14 (𝜑 → (Base‘𝐴) = (Base‘𝐵))
148147sqxpeqd 5065 . . . . . . . . . . . . 13 (𝜑 → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
149148adantr 480 . . . . . . . . . . . 12 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
150149ixpeq1d 7806 . . . . . . . . . . 11 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
151146, 150eqtrd 2644 . . . . . . . . . 10 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
152151eleq2d 2673 . . . . . . . . 9 ((𝜑𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → (𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))))
153152pm5.32da 671 . . . . . . . 8 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))))
1548homfeqbas 16179 . . . . . . . . . 10 (𝜑 → (Base‘𝐶) = (Base‘𝐷))
155147, 154feq23d 5953 . . . . . . . . 9 (𝜑 → (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ↔ 𝑓:(Base‘𝐵)⟶(Base‘𝐷)))
156155anbi1d 737 . . . . . . . 8 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))))
157153, 156bitrd 267 . . . . . . 7 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))))
158147adantr 480 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
159158raleqdv 3121 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
160158, 159raleqbidv 3129 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
161160anbi2d 736 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
162147, 161raleqbidva 3131 . . . . . . 7 (𝜑 → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
163157, 162anbi12d 743 . . . . . 6 (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
164124, 163bitrd 267 . . . . 5 (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
165 df-3an 1033 . . . . 5 ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
166 df-3an 1033 . . . . 5 ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
167164, 165, 1663bitr4g 302 . . . 4 (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
16813, 167anbi12d 743 . . 3 (𝜑 → (((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))) ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))))
169 df-br 4584 . . . . 5 (𝑓(𝐴 Func 𝐶)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶))
170 funcrcl 16346 . . . . 5 (⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶) → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
171169, 170sylbi 206 . . . 4 (𝑓(𝐴 Func 𝐶)𝑔 → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
172 eqid 2610 . . . . 5 (Id‘𝐴) = (Id‘𝐴)
173 eqid 2610 . . . . 5 (Id‘𝐶) = (Id‘𝐶)
174 simpl 472 . . . . 5 ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐴 ∈ Cat)
175 simpr 476 . . . . 5 ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat)
17635, 48, 36, 49, 172, 173, 37, 50, 174, 175isfunc 16347 . . . 4 ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → (𝑓(𝐴 Func 𝐶)𝑔 ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
177171, 176biadan2 672 . . 3 (𝑓(𝐴 Func 𝐶)𝑔 ↔ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st𝑧))(Hom ‘𝐶)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐶)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
178 df-br 4584 . . . . 5 (𝑓(𝐵 Func 𝐷)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷))
179 funcrcl 16346 . . . . 5 (⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷) → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
180178, 179sylbi 206 . . . 4 (𝑓(𝐵 Func 𝐷)𝑔 → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
181 eqid 2610 . . . . 5 (Base‘𝐵) = (Base‘𝐵)
182 eqid 2610 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
183 eqid 2610 . . . . 5 (Id‘𝐵) = (Id‘𝐵)
184 eqid 2610 . . . . 5 (Id‘𝐷) = (Id‘𝐷)
185 simpl 472 . . . . 5 ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐵 ∈ Cat)
186 simpr 476 . . . . 5 ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐷 ∈ Cat)
187181, 182, 109, 125, 183, 184, 38, 51, 185, 186isfunc 16347 . . . 4 ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓(𝐵 Func 𝐷)𝑔 ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
188180, 187biadan2 672 . . 3 (𝑓(𝐵 Func 𝐷)𝑔 ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st𝑧))(Hom ‘𝐷)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝐷)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
189168, 177, 1883bitr4g 302 . 2 (𝜑 → (𝑓(𝐴 Func 𝐶)𝑔𝑓(𝐵 Func 𝐷)𝑔))
1901, 2, 189eqbrrdiv 5141 1 (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ⟨cop 4131   class class class wbr 4583   × cxp 5036  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  Xcixp 7794  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148  Idccid 16149  Homf chomf 16150  compfccomf 16151   Func cfunc 16337 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-ixp 7795  df-cat 16152  df-cid 16153  df-homf 16154  df-comf 16155  df-func 16341 This theorem is referenced by:  funcres2c  16384  fullpropd  16403  fthpropd  16404  ressffth  16421  natpropd  16459  fucpropd  16460  funcsetcres2  16566
 Copyright terms: Public domain W3C validator