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

Theorem funcres 16603
 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 16599 . . 3 (𝜑 → (𝐹f 𝐻) = ⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩)
43fveq2d 6233 . . . . 5 (𝜑 → (2nd ‘(𝐹f 𝐻)) = (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩))
5 fvex 6239 . . . . . . 7 (1st𝐹) ∈ V
65resex 5478 . . . . . 6 ((1st𝐹) ↾ dom dom 𝐻) ∈ V
7 dmexg 7139 . . . . . . 7 (𝐻 ∈ (Subcat‘𝐶) → dom 𝐻 ∈ V)
8 mptexg 6525 . . . . . . 7 (dom 𝐻 ∈ V → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V)
92, 7, 83syl 18 . . . . . 6 (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V)
10 op2ndg 7223 . . . . . 6 ((((1st𝐹) ↾ dom dom 𝐻) ∈ V ∧ (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) ∈ V) → (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
116, 9, 10sylancr 696 . . . . 5 (𝜑 → (2nd ‘⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
124, 11eqtrd 2685 . . . 4 (𝜑 → (2nd ‘(𝐹f 𝐻)) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))))
1312opeq2d 4440 . . 3 (𝜑 → ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ = ⟨((1st𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))⟩)
143, 13eqtr4d 2688 . 2 (𝜑 → (𝐹f 𝐻) = ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩)
15 eqid 2651 . . . 4 (Base‘(𝐶cat 𝐻)) = (Base‘(𝐶cat 𝐻))
16 eqid 2651 . . . 4 (Base‘𝐷) = (Base‘𝐷)
17 eqid 2651 . . . 4 (Hom ‘(𝐶cat 𝐻)) = (Hom ‘(𝐶cat 𝐻))
18 eqid 2651 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
19 eqid 2651 . . . 4 (Id‘(𝐶cat 𝐻)) = (Id‘(𝐶cat 𝐻))
20 eqid 2651 . . . 4 (Id‘𝐷) = (Id‘𝐷)
21 eqid 2651 . . . 4 (comp‘(𝐶cat 𝐻)) = (comp‘(𝐶cat 𝐻))
22 eqid 2651 . . . 4 (comp‘𝐷) = (comp‘𝐷)
23 eqid 2651 . . . . 5 (𝐶cat 𝐻) = (𝐶cat 𝐻)
2423, 2subccat 16555 . . . 4 (𝜑 → (𝐶cat 𝐻) ∈ Cat)
25 funcrcl 16570 . . . . . 6 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
261, 25syl 17 . . . . 5 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
2726simprd 478 . . . 4 (𝜑𝐷 ∈ Cat)
28 eqid 2651 . . . . . . 7 (Base‘𝐶) = (Base‘𝐶)
29 relfunc 16569 . . . . . . . 8 Rel (𝐶 Func 𝐷)
30 1st2ndbr 7261 . . . . . . . 8 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
3129, 1, 30sylancr 696 . . . . . . 7 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
3228, 16, 31funcf1 16573 . . . . . 6 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
33 eqidd 2652 . . . . . . . 8 (𝜑 → dom dom 𝐻 = dom dom 𝐻)
342, 33subcfn 16548 . . . . . . 7 (𝜑𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
352, 34, 28subcss1 16549 . . . . . 6 (𝜑 → dom dom 𝐻 ⊆ (Base‘𝐶))
3632, 35fssresd 6109 . . . . 5 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻):dom dom 𝐻⟶(Base‘𝐷))
3726simpld 474 . . . . . . 7 (𝜑𝐶 ∈ Cat)
3823, 28, 37, 34, 35rescbas 16536 . . . . . 6 (𝜑 → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
3938feq2d 6069 . . . . 5 (𝜑 → (((1st𝐹) ↾ dom dom 𝐻):dom dom 𝐻⟶(Base‘𝐷) ↔ ((1st𝐹) ↾ dom dom 𝐻):(Base‘(𝐶cat 𝐻))⟶(Base‘𝐷)))
4036, 39mpbid 222 . . . 4 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻):(Base‘(𝐶cat 𝐻))⟶(Base‘𝐷))
41 fvex 6239 . . . . . . 7 ((2nd𝐹)‘𝑧) ∈ V
4241resex 5478 . . . . . 6 (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)) ∈ V
43 eqid 2651 . . . . . 6 (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) = (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧)))
4442, 43fnmpti 6060 . . . . 5 (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) Fn dom 𝐻
4512eqcomd 2657 . . . . . 6 (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) = (2nd ‘(𝐹f 𝐻)))
46 fndm 6028 . . . . . . . 8 (𝐻 Fn (dom dom 𝐻 × dom dom 𝐻) → dom 𝐻 = (dom dom 𝐻 × dom dom 𝐻))
4734, 46syl 17 . . . . . . 7 (𝜑 → dom 𝐻 = (dom dom 𝐻 × dom dom 𝐻))
4838sqxpeqd 5175 . . . . . . 7 (𝜑 → (dom dom 𝐻 × dom dom 𝐻) = ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
4947, 48eqtrd 2685 . . . . . 6 (𝜑 → dom 𝐻 = ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
5045, 49fneq12d 6021 . . . . 5 (𝜑 → ((𝑧 ∈ dom 𝐻 ↦ (((2nd𝐹)‘𝑧) ↾ (𝐻𝑧))) Fn dom 𝐻 ↔ (2nd ‘(𝐹f 𝐻)) Fn ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻)))))
5144, 50mpbii 223 . . . 4 (𝜑 → (2nd ‘(𝐹f 𝐻)) Fn ((Base‘(𝐶cat 𝐻)) × (Base‘(𝐶cat 𝐻))))
52 eqid 2651 . . . . . . . 8 (Hom ‘𝐶) = (Hom ‘𝐶)
5331adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
5435adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → dom dom 𝐻 ⊆ (Base‘𝐶))
55 simprl 809 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ (Base‘(𝐶cat 𝐻)))
5638adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
5755, 56eleqtrrd 2733 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ dom dom 𝐻)
5854, 57sseldd 3637 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑥 ∈ (Base‘𝐶))
59 simprr 811 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ (Base‘(𝐶cat 𝐻)))
6059, 56eleqtrrd 2733 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ dom dom 𝐻)
6154, 60sseldd 3637 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝑦 ∈ (Base‘𝐶))
6228, 52, 18, 53, 58, 61funcf2 16575 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
632adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 ∈ (Subcat‘𝐶))
6434adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
6563, 64, 52, 57, 60subcss2 16550 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥𝐻𝑦) ⊆ (𝑥(Hom ‘𝐶)𝑦))
6662, 65fssresd 6109 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
671adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐹 ∈ (𝐶 Func 𝐷))
6867, 63, 64, 57, 60resf2nd 16602 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦) = ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)))
6968feq1d 6068 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ↔ ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦))))
7066, 69mpbird 247 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
7123, 28, 37, 34, 35reschom 16537 . . . . . . . 8 (𝜑𝐻 = (Hom ‘(𝐶cat 𝐻)))
7271adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → 𝐻 = (Hom ‘(𝐶cat 𝐻)))
7372oveqd 6707 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥𝐻𝑦) = (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
74 fvres 6245 . . . . . . . . 9 (𝑥 ∈ dom dom 𝐻 → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
7557, 74syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑥) = ((1st𝐹)‘𝑥))
76 fvres 6245 . . . . . . . . 9 (𝑦 ∈ dom dom 𝐻 → (((1st𝐹) ↾ dom dom 𝐻)‘𝑦) = ((1st𝐹)‘𝑦))
7760, 76syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹) ↾ dom dom 𝐻)‘𝑦) = ((1st𝐹)‘𝑦))
7875, 77oveq12d 6708 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)) = (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
7978eqcomd 2657 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) = ((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)))
8073, 79feq23d 6078 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) ↔ (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥(Hom ‘(𝐶cat 𝐻))𝑦)⟶((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦))))
8170, 80mpbid 222 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦):(𝑥(Hom ‘(𝐶cat 𝐻))𝑦)⟶((((1st𝐹) ↾ dom dom 𝐻)‘𝑥)(Hom ‘𝐷)(((1st𝐹) ↾ dom dom 𝐻)‘𝑦)))
821adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐹 ∈ (𝐶 Func 𝐷))
832adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐻 ∈ (Subcat‘𝐶))
8434adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
8538eleq2d 2716 . . . . . . . 8 (𝜑 → (𝑥 ∈ dom dom 𝐻𝑥 ∈ (Base‘(𝐶cat 𝐻))))
8685biimpar 501 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝑥 ∈ dom dom 𝐻)
8782, 83, 84, 86, 86resf2nd 16602 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑥) = ((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥)))
88 eqid 2651 . . . . . . . 8 (Id‘𝐶) = (Id‘𝐶)
8923, 83, 84, 88, 86subcid 16554 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐶)‘𝑥) = ((Id‘(𝐶cat 𝐻))‘𝑥))
9089eqcomd 2657 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘(𝐶cat 𝐻))‘𝑥) = ((Id‘𝐶)‘𝑥))
9187, 90fveq12d 6235 . . . . 5 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑥)‘((Id‘(𝐶cat 𝐻))‘𝑥)) = (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)))
9231adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
9338, 35eqsstr3d 3673 . . . . . . . 8 (𝜑 → (Base‘(𝐶cat 𝐻)) ⊆ (Base‘𝐶))
9493sselda 3636 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → 𝑥 ∈ (Base‘𝐶))
9528, 88, 20, 92, 94funcid 16577 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
9683, 84, 86, 88subcidcl 16551 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥))
97 fvres 6245 . . . . . . 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 6233 . . . . . 6 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
10195, 98, 1003eqtr4d 2695 . . . . 5 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → (((𝑥(2nd𝐹)𝑥) ↾ (𝑥𝐻𝑥))‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)))
10291, 101eqtrd 2685 . . . 4 ((𝜑𝑥 ∈ (Base‘(𝐶cat 𝐻))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑥)‘((Id‘(𝐶cat 𝐻))‘𝑥)) = ((Id‘𝐷)‘(((1st𝐹) ↾ dom dom 𝐻)‘𝑥)))
10323ad2ant1 1102 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 ∈ (Subcat‘𝐶))
104343ad2ant1 1102 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
105 simp21 1114 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ (Base‘(𝐶cat 𝐻)))
106383ad2ant1 1102 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → dom dom 𝐻 = (Base‘(𝐶cat 𝐻)))
107105, 106eleqtrrd 2733 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ dom dom 𝐻)
108 eqid 2651 . . . . . . . 8 (comp‘𝐶) = (comp‘𝐶)
109 simp22 1115 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ (Base‘(𝐶cat 𝐻)))
110109, 106eleqtrrd 2733 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ dom dom 𝐻)
111 simp23 1116 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ (Base‘(𝐶cat 𝐻)))
112111, 106eleqtrrd 2733 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ dom dom 𝐻)
113 simp3l 1109 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
114713ad2ant1 1102 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐻 = (Hom ‘(𝐶cat 𝐻)))
115114oveqd 6707 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥𝐻𝑦) = (𝑥(Hom ‘(𝐶cat 𝐻))𝑦))
116113, 115eleqtrrd 2733 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥𝐻𝑦))
117 simp3r 1110 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))
118114oveqd 6707 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦𝐻𝑧) = (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))
119117, 118eleqtrrd 2733 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦𝐻𝑧))
120103, 104, 107, 108, 110, 112, 116, 119subccocl 16552 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧))
121 fvres 6245 . . . . . . 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 1102 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
124353ad2ant1 1102 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → dom dom 𝐻 ⊆ (Base‘𝐶))
125124, 107sseldd 3637 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑥 ∈ (Base‘𝐶))
126124, 110sseldd 3637 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑦 ∈ (Base‘𝐶))
127124, 112sseldd 3637 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑧 ∈ (Base‘𝐶))
128103, 104, 52, 107, 110subcss2 16550 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥𝐻𝑦) ⊆ (𝑥(Hom ‘𝐶)𝑦))
129128, 116sseldd 3637 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
130103, 104, 52, 110, 112subcss2 16550 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦𝐻𝑧) ⊆ (𝑦(Hom ‘𝐶)𝑧))
131130, 119sseldd 3637 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
13228, 52, 108, 22, 123, 125, 126, 127, 129, 131funcco 16578 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
133122, 132eqtrd 2685 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
13413ad2ant1 1102 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → 𝐹 ∈ (𝐶 Func 𝐷))
135134, 103, 104, 107, 112resf2nd 16602 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑧) = ((𝑥(2nd𝐹)𝑧) ↾ (𝑥𝐻𝑧)))
13623, 28, 37, 34, 35, 108rescco 16539 . . . . . . . . . 10 (𝜑 → (comp‘𝐶) = (comp‘(𝐶cat 𝐻)))
1371363ad2ant1 1102 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (comp‘𝐶) = (comp‘(𝐶cat 𝐻)))
138137eqcomd 2657 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (comp‘(𝐶cat 𝐻)) = (comp‘𝐶))
139138oveqd 6707 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
140139oveqd 6707 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝐶cat 𝐻))𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
141135, 140fveq12d 6235 . . . . 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 4441 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ⟨(((1st𝐹) ↾ dom dom 𝐻)‘𝑥), (((1st𝐹) ↾ dom dom 𝐻)‘𝑦)⟩ = ⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩)
145 fvres 6245 . . . . . . . 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 6708 . . . . . 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 16602 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑦(2nd ‘(𝐹f 𝐻))𝑧) = ((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧)))
149148fveq1d 6231 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔) = (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔))
150 fvres 6245 . . . . . . . 8 (𝑔 ∈ (𝑦𝐻𝑧) → (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
151119, 150syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑦(2nd𝐹)𝑧) ↾ (𝑦𝐻𝑧))‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
152149, 151eqtrd 2685 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑦(2nd ‘(𝐹f 𝐻))𝑧)‘𝑔) = ((𝑦(2nd𝐹)𝑧)‘𝑔))
153134, 103, 104, 107, 110resf2nd 16602 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (𝑥(2nd ‘(𝐹f 𝐻))𝑦) = ((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦)))
154153fveq1d 6231 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓) = (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓))
155 fvres 6245 . . . . . . . 8 (𝑓 ∈ (𝑥𝐻𝑦) → (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
156116, 155syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → (((𝑥(2nd𝐹)𝑦) ↾ (𝑥𝐻𝑦))‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
157154, 156eqtrd 2685 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑦 ∈ (Base‘(𝐶cat 𝐻)) ∧ 𝑧 ∈ (Base‘(𝐶cat 𝐻))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝐶cat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝐶cat 𝐻))𝑧))) → ((𝑥(2nd ‘(𝐹f 𝐻))𝑦)‘𝑓) = ((𝑥(2nd𝐹)𝑦)‘𝑓))
158147, 152, 157oveq123d 6711 . . . . 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 2695 . . . 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 16572 . . 3 (𝜑 → ((1st𝐹) ↾ dom dom 𝐻)((𝐶cat 𝐻) Func 𝐷)(2nd ‘(𝐹f 𝐻)))
161 df-br 4686 . . 3 (((1st𝐹) ↾ dom dom 𝐻)((𝐶cat 𝐻) Func 𝐷)(2nd ‘(𝐹f 𝐻)) ↔ ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ ∈ ((𝐶cat 𝐻) Func 𝐷))
162160, 161sylib 208 . 2 (𝜑 → ⟨((1st𝐹) ↾ dom dom 𝐻), (2nd ‘(𝐹f 𝐻))⟩ ∈ ((𝐶cat 𝐻) Func 𝐷))
16314, 162eqeltrd 2730 1 (𝜑 → (𝐹f 𝐻) ∈ ((𝐶cat 𝐻) Func 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  Vcvv 3231   ⊆ wss 3607  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  dom cdm 5143   ↾ cres 5145  Rel wrel 5148   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  Basecbs 15904  Hom chom 15999  compcco 16000  Catccat 16372  Idccid 16373   ↾cat cresc 16515  Subcatcsubc 16516   Func cfunc 16561   ↾f cresf 16564 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-hom 16013  df-cco 16014  df-cat 16376  df-cid 16377  df-homf 16378  df-ssc 16517  df-resc 16518  df-subc 16519  df-func 16565  df-resf 16568 This theorem is referenced by:  funcrngcsetc  42323  funcringcsetc  42360
 Copyright terms: Public domain W3C validator