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

Theorem funcres 16821
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 16817 . . 3 (𝜑 → (𝐹f 𝐻) = ⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩)
43fveq2d 6379 . . . . 5 (𝜑 → (2nd ‘(𝐹f 𝐻)) = (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩))
5 fvex 6388 . . . . . . 7 (1st𝐹) ∈ V
65resex 5620 . . . . . 6 ((1st𝐹) ↾ dom dom 𝐻) ∈ V
7 dmexg 7295 . . . . . . 7 (𝐻 ∈ (Subcat‘𝐶) → dom 𝐻 ∈ V)
8 mptexg 6677 . . . . . . 7 (dom 𝐻 ∈ V → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V)
92, 7, 83syl 18 . . . . . 6 (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V)
10 op2ndg 7379 . . . . . 6 ((((1st𝐹) ↾ dom dom 𝐻) ∈ V ∧ (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V) → (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
116, 9, 10sylancr 581 . . . . 5 (𝜑 → (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
124, 11eqtrd 2799 . . . 4 (𝜑 → (2nd ‘(𝐹f 𝐻)) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
1312opeq2d 4566 . . 3 (𝜑 → ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ = ⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩)
143, 13eqtr4d 2802 . 2 (𝜑 → (𝐹f 𝐻) = ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩)
15 eqid 2765 . . . 4 (Base‘(𝐶cat 𝐻)) = (Base‘(𝐶cat 𝐻))
16 eqid 2765 . . . 4 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2765 . . . 4 (Hom ‘(𝐶cat 𝐻)) = (Hom ‘(𝐶cat 𝐻))
18 eqid 2765 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
19 eqid 2765 . . . 4 (Id‘(𝐶cat 𝐻)) = (Id‘(𝐶cat 𝐻))
20 eqid 2765 . . . 4 (Id‘𝐷) = (Id‘𝐷)
21 eqid 2765 . . . 4 (comp‘(𝐶cat 𝐻)) = (comp‘(𝐶cat 𝐻))
22 eqid 2765 . . . 4 (comp‘𝐷) = (comp‘𝐷)
23 eqid 2765 . . . . 5 (𝐶cat 𝐻) = (𝐶cat 𝐻)
2423, 2subccat 16773 . . . 4 (𝜑 → (𝐶cat 𝐻) ∈ Cat)
25 funcrcl 16788 . . . . . 6 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
261, 25syl 17 . . . . 5 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
2726simprd 489 . . . 4 (𝜑𝐷 ∈ Cat)
28 eqid 2765 . . . . . . 7 (Base‘𝐶) = (Base‘𝐶)
29 relfunc 16787 . . . . . . . 8 Rel (𝐶 Func 𝐷)
30 1st2ndbr 7417 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
3129, 1, 30sylancr 581 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
3228, 16, 31funcf1 16791 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
33 eqidd 2766 . . . . . . . 8 (𝜑 → dom dom 𝐻 = dom dom 𝐻)
342, 33subcfn 16766 . . . . . . 7 (𝜑𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
352, 34, 28subcss1 16767 . . . . . 6 (𝜑 → dom dom 𝐻 ⊆ (Base‘𝐶))
3632, 35fssresd 6253 . . . . 5 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻):dom dom 𝐻⟶(Base‘𝐷))
3726simpld 488 . . . . . . 7 (𝜑𝐶 ∈ Cat)
3823, 28, 37, 34, 35rescbas 16754 . . . . . 6 (𝜑 → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
3938feq2d 6209 . . . . 5 (𝜑 → (((1st𝐹) ↾ dom dom 𝐻):dom dom 𝐻⟶(Base‘𝐷) ↔ ((1st𝐹) ↾ dom dom 𝐻):(Base‘(𝐶cat 𝐻))⟶(Base‘𝐷)))
4036, 39mpbid 223 . . . 4 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻):(Base‘(𝐶cat 𝐻))⟶(Base‘𝐷))
41 fvex 6388 . . . . . . 7 ((2nd𝐹)‘𝑧) ∈ V
4241resex 5620 . . . . . 6 (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)) ∈ V
43 eqid 2765 . . . . . 6 (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))
4442, 43fnmpti 6200 . . . . 5 (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) Fn dom 𝐻
4512eqcomd 2771 . . . . . 6 (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) = (2nd ‘(𝐹f 𝐻)))
46 fndm 6168 . . . . . . . 8 (𝐻 Fn (dom dom 𝐻 × dom dom 𝐻) → dom 𝐻 = (dom dom 𝐻 × dom dom 𝐻))
4734, 46syl 17 . . . . . . 7 (𝜑 → dom 𝐻 = (dom dom 𝐻 × dom dom 𝐻))
4838sqxpeqd 5309 . . . . . . 7 (𝜑 → (dom dom 𝐻 × dom dom 𝐻) = ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
4947, 48eqtrd 2799 . . . . . 6 (𝜑 → dom 𝐻 = ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
5045, 49fneq12d 6161 . . . . 5 (𝜑 → ((𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) Fn dom 𝐻 ↔ (2nd ‘(𝐹f 𝐻)) Fn ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻)))))
5144, 50mpbii 224 . . . 4 (𝜑 → (2nd ‘(𝐹f 𝐻)) Fn ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
52 eqid 2765 . . . . . . . 8 (Hom ‘𝐶) = (Hom ‘𝐶)
5331adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
5435adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → dom dom 𝐻 ⊆ (Base‘𝐶))
55 simprl 787 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ (Base‘(𝐶cat 𝐻)))
5638adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
5755, 56eleqtrrd 2847 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ dom dom 𝐻)
5854, 57sseldd 3762 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ (Base‘𝐶))
59 simprr 789 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ (Base‘(𝐶cat 𝐻)))
6059, 56eleqtrrd 2847 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ dom dom 𝐻)
6154, 60sseldd 3762 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ (Base‘𝐶))
6228, 52, 18, 53, 58, 61funcf2 16793 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
632adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 ∈ (Subcat‘𝐶))
6434adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
6563, 64, 52, 57, 60subcss2 16768 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥𝐻𝑦) ⊆ (𝑥(Hom ‘𝐶)𝑦))
6662, 65fssresd 6253 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
671adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐹 ∈ (𝐶 Func 𝐷))
6867, 63, 64, 57, 60resf2nd 16820 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦) = ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)))
6968feq1d 6208 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ↔ ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))))
7066, 69mpbird 248 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
7123, 28, 37, 34, 35reschom 16755 . . . . . . . 8 (𝜑𝐻 = (Hom ‘(𝐶cat 𝐻)))
7271adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 = (Hom ‘(𝐶cat 𝐻)))
7372oveqd 6859 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥𝐻𝑦) = (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
74 fvres 6394 . . . . . . . . 9 (𝑥 ∈ dom dom 𝐻 → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
7557, 74syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
76 fvres 6394 . . . . . . . . 9 (𝑦 ∈ dom dom 𝐻 → (((1st𝐹) ↾ dom dom 𝐻)‘𝑦) = ((1st𝐹)‘𝑦))
7760, 76syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑦) = ((1st𝐹)‘𝑦))
7875, 77oveq12d 6860 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)) = (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
7978eqcomd 2771 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) = ((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)))
8073, 79feq23d 6218 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ↔ (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥(Hom ‘(𝐶cat 𝐻))𝑦)⟶((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦))))
8170, 80mpbid 223 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥(Hom ‘(𝐶cat 𝐻))𝑦)⟶((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)))
821adantr 472 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐹 ∈ (𝐶 Func 𝐷))
832adantr 472 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐻 ∈ (Subcat‘𝐶))
8434adantr 472 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
8538eleq2d 2830 . . . . . . . 8 (𝜑 → (𝑥 ∈ dom dom 𝐻𝑥 ∈ (Base‘(𝐶cat 𝐻))))
8685biimpar 469 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝑥 ∈ dom dom 𝐻)
8782, 83, 84, 86, 86resf2nd 16820 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑥) = ((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥)))
88 eqid 2765 . . . . . . . 8 (Id‘𝐶) = (Id‘𝐶)
8923, 83, 84, 88, 86subcid 16772 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐶)‘𝑥) = ((Id‘(𝐶cat 𝐻))‘𝑥))
9089eqcomd 2771 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘(𝐶cat 𝐻))‘𝑥) = ((Id‘𝐶)‘𝑥))
9187, 90fveq12d 6382 . . . . 5 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑥)‘((Id‘(𝐶cat 𝐻))‘𝑥)) = (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)))
9231adantr 472 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
9338, 35eqsstr3d 3800 . . . . . . . 8 (𝜑 → (Base‘(𝐶cat 𝐻)) ⊆ (Base‘𝐶))
9493sselda 3761 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝑥 ∈ (Base‘𝐶))
9528, 88, 20, 92, 94funcid 16795 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
9683, 84, 86, 88subcidcl 16769 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
97 fvres 6394 . . . . . . 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 6379 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
10195, 98, 1003eqtr4d 2809 . . . . 5 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)))
10291, 101eqtrd 2799 . . . 4 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑥)‘((Id‘(𝐶cat 𝐻))‘𝑥)) = ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)))
10323ad2ant1 1163 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 ∈ (Subcat‘𝐶))
104343ad2ant1 1163 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
105 simp21 1263 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ (Base‘(𝐶cat 𝐻)))
106383ad2ant1 1163 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
107105, 106eleqtrrd 2847 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ dom dom 𝐻)
108 eqid 2765 . . . . . . . 8 (comp‘𝐶) = (comp‘𝐶)
109 simp22 1264 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ (Base‘(𝐶cat 𝐻)))
110109, 106eleqtrrd 2847 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ dom dom 𝐻)
111 simp23 1265 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ (Base‘(𝐶cat 𝐻)))
112111, 106eleqtrrd 2847 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ dom dom 𝐻)
113 simp3l 1258 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
114713ad2ant1 1163 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 = (Hom ‘(𝐶cat 𝐻)))
115114oveqd 6859 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥𝐻𝑦) = (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
116113, 115eleqtrrd 2847 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥𝐻𝑦))
117 simp3r 1259 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))
118114oveqd 6859 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦𝐻𝑧) = (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))
119117, 118eleqtrrd 2847 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦𝐻𝑧))
120103, 104, 107, 108, 110, 112, 116, 119subccocl 16770 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
121 fvres 6394 . . . . . . 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 1163 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
124353ad2ant1 1163 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → dom dom 𝐻 ⊆ (Base‘𝐶))
125124, 107sseldd 3762 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ (Base‘𝐶))
126124, 110sseldd 3762 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ (Base‘𝐶))
127124, 112sseldd 3762 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ (Base‘𝐶))
128103, 104, 52, 107, 110subcss2 16768 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥𝐻𝑦) ⊆ (𝑥(Hom ‘𝐶)𝑦))
129128, 116sseldd 3762 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
130103, 104, 52, 110, 112subcss2 16768 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦𝐻𝑧) ⊆ (𝑦(Hom ‘𝐶)𝑧))
131130, 119sseldd 3762 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
13228, 52, 108, 22, 123, 125, 126, 127, 129, 131funcco 16796 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
133122, 132eqtrd 2799 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
13413ad2ant1 1163 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐹 ∈ (𝐶 Func 𝐷))
135134, 103, 104, 107, 112resf2nd 16820 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑧) = ((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧)))
13623, 28, 37, 34, 35, 108rescco 16757 . . . . . . . . . 10 (𝜑 → (comp‘𝐶) = (comp‘(𝐶cat 𝐻)))
1371363ad2ant1 1163 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (comp‘𝐶) = (comp‘(𝐶cat 𝐻)))
138137eqcomd 2771 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (comp‘(𝐶cat 𝐻)) = (comp‘𝐶))
139138oveqd 6859 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
140139oveqd 6859 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
141135, 140fveq12d 6382 . . . . 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 4567 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ⟨(((1st𝐹) ↾ dom dom 𝐻)‘𝑥), (((1st𝐹) ↾ dom dom 𝐻)‘𝑦)⟩ = ⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩)
145 fvres 6394 . . . . . . . 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 6860 . . . . . 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 16820 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦(2nd ‘(𝐹f 𝐻))𝑧) = ((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧)))
149148fveq1d 6377 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔) = (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔))
150 fvres 6394 . . . . . . . 8 (𝑔 ∈ (𝑦𝐻𝑧) → (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
151119, 150syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
152149, 151eqtrd 2799 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
153134, 103, 104, 107, 110resf2nd 16820 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦) = ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)))
154153fveq1d 6377 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓) = (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓))
155 fvres 6394 . . . . . . . 8 (𝑓 ∈ (𝑥𝐻𝑦) → (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
156116, 155syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
157154, 156eqtrd 2799 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
158147, 152, 157oveq123d 6863 . . . . 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 2809 . . . 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 16790 . . 3 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻)((𝐶cat 𝐻) Func 𝐷)(2nd ‘(𝐹f 𝐻)))
161 df-br 4810 . . 3 (((1st𝐹) ↾ dom dom 𝐻)((𝐶cat 𝐻) Func 𝐷)(2nd ‘(𝐹f 𝐻)) ↔ ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ ∈ ((𝐶cat 𝐻) Func 𝐷))
162160, 161sylib 209 . 2 (𝜑 → ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ ∈ ((𝐶cat 𝐻) Func 𝐷))
16314, 162eqeltrd 2844 1 (𝜑 → (𝐹f 𝐻) ∈ ((𝐶cat 𝐻) Func 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107   = wceq 1652  wcel 2155  Vcvv 3350  wss 3732  cop 4340   class class class wbr 4809  cmpt 4888   × cxp 5275  dom cdm 5277  cres 5279  Rel wrel 5282   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  1st c1st 7364  2nd c2nd 7365  Basecbs 16130  Hom chom 16225  compcco 16226  Catccat 16590  Idccid 16591  cat cresc 16733  Subcatcsubc 16734   Func cfunc 16779  f cresf 16782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-hom 16238  df-cco 16239  df-cat 16594  df-cid 16595  df-homf 16596  df-ssc 16735  df-resc 16736  df-subc 16737  df-func 16783  df-resf 16786
This theorem is referenced by:  funcrngcsetc  42667  funcringcsetc  42704
  Copyright terms: Public domain W3C validator