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

Theorem funcres 16327
Description: A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
funcres.f (𝜑𝐹 ∈ (𝐶 Func 𝐷))
funcres.h (𝜑𝐻 ∈ (Subcat‘𝐶))
Assertion
Ref Expression
funcres (𝜑 → (𝐹f 𝐻) ∈ ((𝐶cat 𝐻) Func 𝐷))

Proof of Theorem funcres
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funcres.f . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
2 funcres.h . . . 4 (𝜑𝐻 ∈ (Subcat‘𝐶))
31, 2resfval 16323 . . 3 (𝜑 → (𝐹f 𝐻) = ⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩)
43fveq2d 6091 . . . . 5 (𝜑 → (2nd ‘(𝐹f 𝐻)) = (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩))
5 fvex 6097 . . . . . . 7 (1st𝐹) ∈ V
65resex 5349 . . . . . 6 ((1st𝐹) ↾ dom dom 𝐻) ∈ V
7 dmexg 6966 . . . . . . 7 (𝐻 ∈ (Subcat‘𝐶) → dom 𝐻 ∈ V)
8 mptexg 6366 . . . . . . 7 (dom 𝐻 ∈ V → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V)
92, 7, 83syl 18 . . . . . 6 (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V)
10 op2ndg 7049 . . . . . 6 ((((1st𝐹) ↾ dom dom 𝐻) ∈ V ∧ (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V) → (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
116, 9, 10sylancr 693 . . . . 5 (𝜑 → (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
124, 11eqtrd 2643 . . . 4 (𝜑 → (2nd ‘(𝐹f 𝐻)) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
1312opeq2d 4341 . . 3 (𝜑 → ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ = ⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩)
143, 13eqtr4d 2646 . 2 (𝜑 → (𝐹f 𝐻) = ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩)
15 eqid 2609 . . . 4 (Base‘(𝐶cat 𝐻)) = (Base‘(𝐶cat 𝐻))
16 eqid 2609 . . . 4 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2609 . . . 4 (Hom ‘(𝐶cat 𝐻)) = (Hom ‘(𝐶cat 𝐻))
18 eqid 2609 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
19 eqid 2609 . . . 4 (Id‘(𝐶cat 𝐻)) = (Id‘(𝐶cat 𝐻))
20 eqid 2609 . . . 4 (Id‘𝐷) = (Id‘𝐷)
21 eqid 2609 . . . 4 (comp‘(𝐶cat 𝐻)) = (comp‘(𝐶cat 𝐻))
22 eqid 2609 . . . 4 (comp‘𝐷) = (comp‘𝐷)
23 eqid 2609 . . . . 5 (𝐶cat 𝐻) = (𝐶cat 𝐻)
2423, 2subccat 16279 . . . 4 (𝜑 → (𝐶cat 𝐻) ∈ Cat)
25 funcrcl 16294 . . . . . 6 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
261, 25syl 17 . . . . 5 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
2726simprd 477 . . . 4 (𝜑𝐷 ∈ Cat)
28 eqid 2609 . . . . . . 7 (Base‘𝐶) = (Base‘𝐶)
29 relfunc 16293 . . . . . . . 8 Rel (𝐶 Func 𝐷)
30 1st2ndbr 7085 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
3129, 1, 30sylancr 693 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
3228, 16, 31funcf1 16297 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
33 eqidd 2610 . . . . . . . 8 (𝜑 → dom dom 𝐻 = dom dom 𝐻)
342, 33subcfn 16272 . . . . . . 7 (𝜑𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
352, 34, 28subcss1 16273 . . . . . 6 (𝜑 → dom dom 𝐻 ⊆ (Base‘𝐶))
3632, 35fssresd 5968 . . . . 5 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻):dom dom 𝐻⟶(Base‘𝐷))
3726simpld 473 . . . . . . 7 (𝜑𝐶 ∈ Cat)
3823, 28, 37, 34, 35rescbas 16260 . . . . . 6 (𝜑 → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
3938feq2d 5929 . . . . 5 (𝜑 → (((1st𝐹) ↾ dom dom 𝐻):dom dom 𝐻⟶(Base‘𝐷) ↔ ((1st𝐹) ↾ dom dom 𝐻):(Base‘(𝐶cat 𝐻))⟶(Base‘𝐷)))
4036, 39mpbid 220 . . . 4 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻):(Base‘(𝐶cat 𝐻))⟶(Base‘𝐷))
41 fvex 6097 . . . . . . 7 ((2nd𝐹)‘𝑧) ∈ V
4241resex 5349 . . . . . 6 (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)) ∈ V
43 eqid 2609 . . . . . 6 (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))
4442, 43fnmpti 5920 . . . . 5 (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) Fn dom 𝐻
4512eqcomd 2615 . . . . . 6 (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) = (2nd ‘(𝐹f 𝐻)))
46 fndm 5889 . . . . . . . 8 (𝐻 Fn (dom dom 𝐻 × dom dom 𝐻) → dom 𝐻 = (dom dom 𝐻 × dom dom 𝐻))
4734, 46syl 17 . . . . . . 7 (𝜑 → dom 𝐻 = (dom dom 𝐻 × dom dom 𝐻))
4838sqxpeqd 5054 . . . . . . 7 (𝜑 → (dom dom 𝐻 × dom dom 𝐻) = ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
4947, 48eqtrd 2643 . . . . . 6 (𝜑 → dom 𝐻 = ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
5045, 49fneq12d 5882 . . . . 5 (𝜑 → ((𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) Fn dom 𝐻 ↔ (2nd ‘(𝐹f 𝐻)) Fn ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻)))))
5144, 50mpbii 221 . . . 4 (𝜑 → (2nd ‘(𝐹f 𝐻)) Fn ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
52 eqid 2609 . . . . . . . 8 (Hom ‘𝐶) = (Hom ‘𝐶)
5331adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
5435adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → dom dom 𝐻 ⊆ (Base‘𝐶))
55 simprl 789 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ (Base‘(𝐶cat 𝐻)))
5638adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
5755, 56eleqtrrd 2690 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ dom dom 𝐻)
5854, 57sseldd 3568 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ (Base‘𝐶))
59 simprr 791 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ (Base‘(𝐶cat 𝐻)))
6059, 56eleqtrrd 2690 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ dom dom 𝐻)
6154, 60sseldd 3568 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ (Base‘𝐶))
6228, 52, 18, 53, 58, 61funcf2 16299 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
632adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 ∈ (Subcat‘𝐶))
6434adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
6563, 64, 52, 57, 60subcss2 16274 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥𝐻𝑦) ⊆ (𝑥(Hom ‘𝐶)𝑦))
6662, 65fssresd 5968 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
671adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐹 ∈ (𝐶 Func 𝐷))
6867, 63, 64, 57, 60resf2nd 16326 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦) = ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)))
6968feq1d 5928 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ↔ ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))))
7066, 69mpbird 245 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
7123, 28, 37, 34, 35reschom 16261 . . . . . . . 8 (𝜑𝐻 = (Hom ‘(𝐶cat 𝐻)))
7271adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 = (Hom ‘(𝐶cat 𝐻)))
7372oveqd 6543 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥𝐻𝑦) = (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
74 fvres 6101 . . . . . . . . 9 (𝑥 ∈ dom dom 𝐻 → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
7557, 74syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
76 fvres 6101 . . . . . . . . 9 (𝑦 ∈ dom dom 𝐻 → (((1st𝐹) ↾ dom dom 𝐻)‘𝑦) = ((1st𝐹)‘𝑦))
7760, 76syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑦) = ((1st𝐹)‘𝑦))
7875, 77oveq12d 6544 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)) = (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
7978eqcomd 2615 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) = ((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)))
8073, 79feq23d 5938 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ↔ (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥(Hom ‘(𝐶cat 𝐻))𝑦)⟶((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦))))
8170, 80mpbid 220 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥(Hom ‘(𝐶cat 𝐻))𝑦)⟶((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)))
821adantr 479 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐹 ∈ (𝐶 Func 𝐷))
832adantr 479 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐻 ∈ (Subcat‘𝐶))
8434adantr 479 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
8538eleq2d 2672 . . . . . . . 8 (𝜑 → (𝑥 ∈ dom dom 𝐻𝑥 ∈ (Base‘(𝐶cat 𝐻))))
8685biimpar 500 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝑥 ∈ dom dom 𝐻)
8782, 83, 84, 86, 86resf2nd 16326 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑥) = ((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥)))
88 eqid 2609 . . . . . . . 8 (Id‘𝐶) = (Id‘𝐶)
8923, 83, 84, 88, 86subcid 16278 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐶)‘𝑥) = ((Id‘(𝐶cat 𝐻))‘𝑥))
9089eqcomd 2615 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘(𝐶cat 𝐻))‘𝑥) = ((Id‘𝐶)‘𝑥))
9187, 90fveq12d 6093 . . . . 5 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑥)‘((Id‘(𝐶cat 𝐻))‘𝑥)) = (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)))
9231adantr 479 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
9338, 35eqsstr3d 3602 . . . . . . . 8 (𝜑 → (Base‘(𝐶cat 𝐻)) ⊆ (Base‘𝐶))
9493sselda 3567 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝑥 ∈ (Base‘𝐶))
9528, 88, 20, 92, 94funcid 16301 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
9683, 84, 86, 88subcidcl 16275 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
97 fvres 6101 . . . . . . 7 (((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥) → (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)) = ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)))
9896, 97syl 17 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)) = ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)))
9986, 74syl 17 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
10099fveq2d 6091 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
10195, 98, 1003eqtr4d 2653 . . . . 5 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)))
10291, 101eqtrd 2643 . . . 4 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑥)‘((Id‘(𝐶cat 𝐻))‘𝑥)) = ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)))
10323ad2ant1 1074 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 ∈ (Subcat‘𝐶))
104343ad2ant1 1074 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
105 simp21 1086 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ (Base‘(𝐶cat 𝐻)))
106383ad2ant1 1074 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
107105, 106eleqtrrd 2690 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ dom dom 𝐻)
108 eqid 2609 . . . . . . . 8 (comp‘𝐶) = (comp‘𝐶)
109 simp22 1087 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ (Base‘(𝐶cat 𝐻)))
110109, 106eleqtrrd 2690 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ dom dom 𝐻)
111 simp23 1088 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ (Base‘(𝐶cat 𝐻)))
112111, 106eleqtrrd 2690 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ dom dom 𝐻)
113 simp3l 1081 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
114713ad2ant1 1074 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 = (Hom ‘(𝐶cat 𝐻)))
115114oveqd 6543 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥𝐻𝑦) = (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
116113, 115eleqtrrd 2690 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥𝐻𝑦))
117 simp3r 1082 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))
118114oveqd 6543 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦𝐻𝑧) = (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))
119117, 118eleqtrrd 2690 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦𝐻𝑧))
120103, 104, 107, 108, 110, 112, 116, 119subccocl 16276 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
121 fvres 6101 . . . . . . 7 ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧) → (((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
122120, 121syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
123313ad2ant1 1074 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
124353ad2ant1 1074 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → dom dom 𝐻 ⊆ (Base‘𝐶))
125124, 107sseldd 3568 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ (Base‘𝐶))
126124, 110sseldd 3568 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ (Base‘𝐶))
127124, 112sseldd 3568 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ (Base‘𝐶))
128103, 104, 52, 107, 110subcss2 16274 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥𝐻𝑦) ⊆ (𝑥(Hom ‘𝐶)𝑦))
129128, 116sseldd 3568 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
130103, 104, 52, 110, 112subcss2 16274 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦𝐻𝑧) ⊆ (𝑦(Hom ‘𝐶)𝑧))
131130, 119sseldd 3568 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
13228, 52, 108, 22, 123, 125, 126, 127, 129, 131funcco 16302 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
133122, 132eqtrd 2643 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
13413ad2ant1 1074 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐹 ∈ (𝐶 Func 𝐷))
135134, 103, 104, 107, 112resf2nd 16326 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑧) = ((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧)))
13623, 28, 37, 34, 35, 108rescco 16263 . . . . . . . . . 10 (𝜑 → (comp‘𝐶) = (comp‘(𝐶cat 𝐻)))
1371363ad2ant1 1074 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (comp‘𝐶) = (comp‘(𝐶cat 𝐻)))
138137eqcomd 2615 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (comp‘(𝐶cat 𝐻)) = (comp‘𝐶))
139138oveqd 6543 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
140139oveqd 6543 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
141135, 140fveq12d 6093 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧)𝑓)) = (((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
142107, 74syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
143110, 76syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑦) = ((1st𝐹)‘𝑦))
144142, 143opeq12d 4342 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ⟨(((1st𝐹) ↾ dom dom 𝐻)‘𝑥), (((1st𝐹) ↾ dom dom 𝐻)‘𝑦)⟩ = ⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩)
145 fvres 6101 . . . . . . . 8 (𝑧 ∈ dom dom 𝐻 → (((1st𝐹) ↾ dom dom 𝐻)‘𝑧) = ((1st𝐹)‘𝑧))
146112, 145syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑧) = ((1st𝐹)‘𝑧))
147144, 146oveq12d 6544 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (⟨(((1st𝐹) ↾ dom dom 𝐻)‘𝑥), (((1st𝐹) ↾ dom dom 𝐻)‘𝑦)⟩(comp‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑧)) = (⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧)))
148134, 103, 104, 110, 112resf2nd 16326 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦(2nd ‘(𝐹f 𝐻))𝑧) = ((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧)))
149148fveq1d 6089 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔) = (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔))
150 fvres 6101 . . . . . . . 8 (𝑔 ∈ (𝑦𝐻𝑧) → (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
151119, 150syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
152149, 151eqtrd 2643 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
153134, 103, 104, 107, 110resf2nd 16326 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦) = ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)))
154153fveq1d 6089 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓) = (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓))
155 fvres 6101 . . . . . . . 8 (𝑓 ∈ (𝑥𝐻𝑦) → (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
156116, 155syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
157154, 156eqtrd 2643 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
158147, 152, 157oveq123d 6547 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔)(⟨(((1st𝐹) ↾ dom dom 𝐻)‘𝑥), (((1st𝐹) ↾ dom dom 𝐻)‘𝑦)⟩(comp‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑧))((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
159133, 141, 1583eqtr4d 2653 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧)𝑓)) = (((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔)(⟨(((1st𝐹) ↾ dom dom 𝐻)‘𝑥), (((1st𝐹) ↾ dom dom 𝐻)‘𝑦)⟩(comp‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑧))((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓)))
16015, 16, 17, 18, 19, 20, 21, 22, 24, 27, 40, 51, 81, 102, 159isfuncd 16296 . . 3 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻)((𝐶cat 𝐻) Func 𝐷)(2nd ‘(𝐹f 𝐻)))
161 df-br 4578 . . 3 (((1st𝐹) ↾ dom dom 𝐻)((𝐶cat 𝐻) Func 𝐷)(2nd ‘(𝐹f 𝐻)) ↔ ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ ∈ ((𝐶cat 𝐻) Func 𝐷))
162160, 161sylib 206 . 2 (𝜑 → ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ ∈ ((𝐶cat 𝐻) Func 𝐷))
16314, 162eqeltrd 2687 1 (𝜑 → (𝐹f 𝐻) ∈ ((𝐶cat 𝐻) Func 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1976  Vcvv 3172  wss 3539  cop 4130   class class class wbr 4577  cmpt 4637   × cxp 5025  dom cdm 5027  cres 5029  Rel wrel 5032   Fn wfn 5784  wf 5785  cfv 5789  (class class class)co 6526  1st c1st 7034  2nd c2nd 7035  Basecbs 15643  Hom chom 15727  compcco 15728  Catccat 16096  Idccid 16097  cat cresc 16239  Subcatcsubc 16240   Func cfunc 16285  f cresf 16288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-5 10931  df-6 10932  df-7 10933  df-8 10934  df-9 10935  df-n0 11142  df-z 11213  df-dec 11328  df-ndx 15646  df-slot 15647  df-base 15648  df-sets 15649  df-ress 15650  df-hom 15741  df-cco 15742  df-cat 16100  df-cid 16101  df-homf 16102  df-ssc 16241  df-resc 16242  df-subc 16243  df-func 16289  df-resf 16292
This theorem is referenced by:  funcrngcsetc  41771  funcringcsetc  41808
  Copyright terms: Public domain W3C validator