MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funcres Structured version   Visualization version   GIF version
Theorem funcres 17842
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 17838 . . 3 (πœ‘ β†’ (𝐹 β†Ύf 𝐻) = ⟨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§)))⟩)
43fveq2d 6892 . . . . 5 (πœ‘ β†’ (2nd β€˜(𝐹 β†Ύf 𝐻)) = (2nd β€˜βŸ¨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§)))⟩))
5 fvex 6901 . . . . . . 7 (1st β€˜πΉ) ∈ V
65resex 6027 . . . . . 6 ((1st β€˜πΉ) β†Ύ dom dom 𝐻) ∈ V
7 dmexg 7890 . . . . . . 7 (𝐻 ∈ (Subcatβ€˜πΆ) β†’ dom 𝐻 ∈ V)
8 mptexg 7219 . . . . . . 7 (dom 𝐻 ∈ V β†’ (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))) ∈ V)
92, 7, 83syl 18 . . . . . 6 (πœ‘ β†’ (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))) ∈ V)
10 op2ndg 7984 . . . . . 6 ((((1st β€˜πΉ) β†Ύ dom dom 𝐻) ∈ V ∧ (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))) ∈ V) β†’ (2nd β€˜βŸ¨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))))
116, 9, 10sylancr 587 . . . . 5 (πœ‘ β†’ (2nd β€˜βŸ¨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§)))⟩) = (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))))
124, 11eqtrd 2772 . . . 4 (πœ‘ β†’ (2nd β€˜(𝐹 β†Ύf 𝐻)) = (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))))
1312opeq2d 4879 . . 3 (πœ‘ β†’ ⟨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (2nd β€˜(𝐹 β†Ύf 𝐻))⟩ = ⟨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§)))⟩)
143, 13eqtr4d 2775 . 2 (πœ‘ β†’ (𝐹 β†Ύf 𝐻) = ⟨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (2nd β€˜(𝐹 β†Ύf 𝐻))⟩)
15 eqid 2732 . . . 4 (Baseβ€˜(𝐢 β†Ύcat 𝐻)) = (Baseβ€˜(𝐢 β†Ύcat 𝐻))
16 eqid 2732 . . . 4 (Baseβ€˜π·) = (Baseβ€˜π·)
17 eqid 2732 . . . 4 (Hom β€˜(𝐢 β†Ύcat 𝐻)) = (Hom β€˜(𝐢 β†Ύcat 𝐻))
18 eqid 2732 . . . 4 (Hom β€˜π·) = (Hom β€˜π·)
19 eqid 2732 . . . 4 (Idβ€˜(𝐢 β†Ύcat 𝐻)) = (Idβ€˜(𝐢 β†Ύcat 𝐻))
20 eqid 2732 . . . 4 (Idβ€˜π·) = (Idβ€˜π·)
21 eqid 2732 . . . 4 (compβ€˜(𝐢 β†Ύcat 𝐻)) = (compβ€˜(𝐢 β†Ύcat 𝐻))
22 eqid 2732 . . . 4 (compβ€˜π·) = (compβ€˜π·)
23 eqid 2732 . . . . 5 (𝐢 β†Ύcat 𝐻) = (𝐢 β†Ύcat 𝐻)
2423, 2subccat 17794 . . . 4 (πœ‘ β†’ (𝐢 β†Ύcat 𝐻) ∈ Cat)
25 funcrcl 17809 . . . . . 6 (𝐹 ∈ (𝐢 Func 𝐷) β†’ (𝐢 ∈ Cat ∧ 𝐷 ∈ Cat))
261, 25syl 17 . . . . 5 (πœ‘ β†’ (𝐢 ∈ Cat ∧ 𝐷 ∈ Cat))
2726simprd 496 . . . 4 (πœ‘ β†’ 𝐷 ∈ Cat)
28 eqid 2732 . . . . . . 7 (Baseβ€˜πΆ) = (Baseβ€˜πΆ)
29 relfunc 17808 . . . . . . . 8 Rel (𝐢 Func 𝐷)
30 1st2ndbr 8024 . . . . . . . 8 ((Rel (𝐢 Func 𝐷) ∧ 𝐹 ∈ (𝐢 Func 𝐷)) β†’ (1st β€˜πΉ)(𝐢 Func 𝐷)(2nd β€˜πΉ))
3129, 1, 30sylancr 587 . . . . . . 7 (πœ‘ β†’ (1st β€˜πΉ)(𝐢 Func 𝐷)(2nd β€˜πΉ))
3228, 16, 31funcf1 17812 . . . . . 6 (πœ‘ β†’ (1st β€˜πΉ):(Baseβ€˜πΆ)⟢(Baseβ€˜π·))
33 eqidd 2733 . . . . . . . 8 (πœ‘ β†’ dom dom 𝐻 = dom dom 𝐻)
342, 33subcfn 17787 . . . . . . 7 (πœ‘ β†’ 𝐻 Fn (dom dom 𝐻 Γ— dom dom 𝐻))
352, 34, 28subcss1 17788 . . . . . 6 (πœ‘ β†’ dom dom 𝐻 βŠ† (Baseβ€˜πΆ))
3632, 35fssresd 6755 . . . . 5 (πœ‘ β†’ ((1st β€˜πΉ) β†Ύ dom dom 𝐻):dom dom 𝐻⟢(Baseβ€˜π·))
3726simpld 495 . . . . . . 7 (πœ‘ β†’ 𝐢 ∈ Cat)
3823, 28, 37, 34, 35rescbas 17772 . . . . . 6 (πœ‘ β†’ dom dom 𝐻 = (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
3938feq2d 6700 . . . . 5 (πœ‘ β†’ (((1st β€˜πΉ) β†Ύ dom dom 𝐻):dom dom 𝐻⟢(Baseβ€˜π·) ↔ ((1st β€˜πΉ) β†Ύ dom dom 𝐻):(Baseβ€˜(𝐢 β†Ύcat 𝐻))⟢(Baseβ€˜π·)))
4036, 39mpbid 231 . . . 4 (πœ‘ β†’ ((1st β€˜πΉ) β†Ύ dom dom 𝐻):(Baseβ€˜(𝐢 β†Ύcat 𝐻))⟢(Baseβ€˜π·))
41 fvex 6901 . . . . . . 7 ((2nd β€˜πΉ)β€˜π‘§) ∈ V
4241resex 6027 . . . . . 6 (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§)) ∈ V
43 eqid 2732 . . . . . 6 (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))) = (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§)))
4442, 43fnmpti 6690 . . . . 5 (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))) Fn dom 𝐻
4512eqcomd 2738 . . . . . 6 (πœ‘ β†’ (𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))) = (2nd β€˜(𝐹 β†Ύf 𝐻)))
46 fndm 6649 . . . . . . . 8 (𝐻 Fn (dom dom 𝐻 Γ— dom dom 𝐻) β†’ dom 𝐻 = (dom dom 𝐻 Γ— dom dom 𝐻))
4734, 46syl 17 . . . . . . 7 (πœ‘ β†’ dom 𝐻 = (dom dom 𝐻 Γ— dom dom 𝐻))
4838sqxpeqd 5707 . . . . . . 7 (πœ‘ β†’ (dom dom 𝐻 Γ— dom dom 𝐻) = ((Baseβ€˜(𝐢 β†Ύcat 𝐻)) Γ— (Baseβ€˜(𝐢 β†Ύcat 𝐻))))
4947, 48eqtrd 2772 . . . . . 6 (πœ‘ β†’ dom 𝐻 = ((Baseβ€˜(𝐢 β†Ύcat 𝐻)) Γ— (Baseβ€˜(𝐢 β†Ύcat 𝐻))))
5045, 49fneq12d 6641 . . . . 5 (πœ‘ β†’ ((𝑧 ∈ dom 𝐻 ↦ (((2nd β€˜πΉ)β€˜π‘§) β†Ύ (π»β€˜π‘§))) Fn dom 𝐻 ↔ (2nd β€˜(𝐹 β†Ύf 𝐻)) Fn ((Baseβ€˜(𝐢 β†Ύcat 𝐻)) Γ— (Baseβ€˜(𝐢 β†Ύcat 𝐻)))))
5144, 50mpbii 232 . . . 4 (πœ‘ β†’ (2nd β€˜(𝐹 β†Ύf 𝐻)) Fn ((Baseβ€˜(𝐢 β†Ύcat 𝐻)) Γ— (Baseβ€˜(𝐢 β†Ύcat 𝐻))))
52 eqid 2732 . . . . . . . 8 (Hom β€˜πΆ) = (Hom β€˜πΆ)
5331adantr 481 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (1st β€˜πΉ)(𝐢 Func 𝐷)(2nd β€˜πΉ))
5435adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ dom dom 𝐻 βŠ† (Baseβ€˜πΆ))
55 simprl 769 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
5638adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ dom dom 𝐻 = (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
5755, 56eleqtrrd 2836 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ π‘₯ ∈ dom dom 𝐻)
5854, 57sseldd 3982 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ π‘₯ ∈ (Baseβ€˜πΆ))
59 simprr 771 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
6059, 56eleqtrrd 2836 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ 𝑦 ∈ dom dom 𝐻)
6154, 60sseldd 3982 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ 𝑦 ∈ (Baseβ€˜πΆ))
6228, 52, 18, 53, 58, 61funcf2 17814 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (π‘₯(2nd β€˜πΉ)𝑦):(π‘₯(Hom β€˜πΆ)𝑦)⟢(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦)))
632adantr 481 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ 𝐻 ∈ (Subcatβ€˜πΆ))
6434adantr 481 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ 𝐻 Fn (dom dom 𝐻 Γ— dom dom 𝐻))
6563, 64, 52, 57, 60subcss2 17789 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (π‘₯𝐻𝑦) βŠ† (π‘₯(Hom β€˜πΆ)𝑦))
6662, 65fssresd 6755 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ ((π‘₯(2nd β€˜πΉ)𝑦) β†Ύ (π‘₯𝐻𝑦)):(π‘₯𝐻𝑦)⟢(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦)))
671adantr 481 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ 𝐹 ∈ (𝐢 Func 𝐷))
6867, 63, 64, 57, 60resf2nd 17841 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦) = ((π‘₯(2nd β€˜πΉ)𝑦) β†Ύ (π‘₯𝐻𝑦)))
6968feq1d 6699 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ ((π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦):(π‘₯𝐻𝑦)⟢(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦)) ↔ ((π‘₯(2nd β€˜πΉ)𝑦) β†Ύ (π‘₯𝐻𝑦)):(π‘₯𝐻𝑦)⟢(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦))))
7066, 69mpbird 256 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦):(π‘₯𝐻𝑦)⟢(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦)))
7123, 28, 37, 34, 35reschom 17774 . . . . . . . 8 (πœ‘ β†’ 𝐻 = (Hom β€˜(𝐢 β†Ύcat 𝐻)))
7271adantr 481 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ 𝐻 = (Hom β€˜(𝐢 β†Ύcat 𝐻)))
7372oveqd 7422 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (π‘₯𝐻𝑦) = (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦))
7457fvresd 6908 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯) = ((1st β€˜πΉ)β€˜π‘₯))
7560fvresd 6908 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘¦) = ((1st β€˜πΉ)β€˜π‘¦))
7674, 75oveq12d 7423 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ ((((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯)(Hom β€˜π·)(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘¦)) = (((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦)))
7776eqcomd 2738 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦)) = ((((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯)(Hom β€˜π·)(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘¦)))
7873, 77feq23d 6709 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ ((π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦):(π‘₯𝐻𝑦)⟢(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π·)((1st β€˜πΉ)β€˜π‘¦)) ↔ (π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦):(π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦)⟢((((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯)(Hom β€˜π·)(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘¦))))
7970, 78mpbid 231 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))) β†’ (π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦):(π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦)⟢((((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯)(Hom β€˜π·)(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘¦)))
801adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ 𝐹 ∈ (𝐢 Func 𝐷))
812adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ 𝐻 ∈ (Subcatβ€˜πΆ))
8234adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ 𝐻 Fn (dom dom 𝐻 Γ— dom dom 𝐻))
8338eleq2d 2819 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ dom dom 𝐻 ↔ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))))
8483biimpar 478 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ π‘₯ ∈ dom dom 𝐻)
8580, 81, 82, 84, 84resf2nd 17841 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ (π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))π‘₯) = ((π‘₯(2nd β€˜πΉ)π‘₯) β†Ύ (π‘₯𝐻π‘₯)))
86 eqid 2732 . . . . . . . 8 (Idβ€˜πΆ) = (Idβ€˜πΆ)
8723, 81, 82, 86, 84subcid 17793 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ ((Idβ€˜πΆ)β€˜π‘₯) = ((Idβ€˜(𝐢 β†Ύcat 𝐻))β€˜π‘₯))
8887eqcomd 2738 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ ((Idβ€˜(𝐢 β†Ύcat 𝐻))β€˜π‘₯) = ((Idβ€˜πΆ)β€˜π‘₯))
8985, 88fveq12d 6895 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ ((π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))π‘₯)β€˜((Idβ€˜(𝐢 β†Ύcat 𝐻))β€˜π‘₯)) = (((π‘₯(2nd β€˜πΉ)π‘₯) β†Ύ (π‘₯𝐻π‘₯))β€˜((Idβ€˜πΆ)β€˜π‘₯)))
9031adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ (1st β€˜πΉ)(𝐢 Func 𝐷)(2nd β€˜πΉ))
9138, 35eqsstrrd 4020 . . . . . . . 8 (πœ‘ β†’ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) βŠ† (Baseβ€˜πΆ))
9291sselda 3981 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ π‘₯ ∈ (Baseβ€˜πΆ))
9328, 86, 20, 90, 92funcid 17816 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ ((π‘₯(2nd β€˜πΉ)π‘₯)β€˜((Idβ€˜πΆ)β€˜π‘₯)) = ((Idβ€˜π·)β€˜((1st β€˜πΉ)β€˜π‘₯)))
9481, 82, 84, 86subcidcl 17790 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ ((Idβ€˜πΆ)β€˜π‘₯) ∈ (π‘₯𝐻π‘₯))
9594fvresd 6908 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ (((π‘₯(2nd β€˜πΉ)π‘₯) β†Ύ (π‘₯𝐻π‘₯))β€˜((Idβ€˜πΆ)β€˜π‘₯)) = ((π‘₯(2nd β€˜πΉ)π‘₯)β€˜((Idβ€˜πΆ)β€˜π‘₯)))
9684fvresd 6908 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ (((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯) = ((1st β€˜πΉ)β€˜π‘₯))
9796fveq2d 6892 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ ((Idβ€˜π·)β€˜(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯)) = ((Idβ€˜π·)β€˜((1st β€˜πΉ)β€˜π‘₯)))
9893, 95, 973eqtr4d 2782 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ (((π‘₯(2nd β€˜πΉ)π‘₯) β†Ύ (π‘₯𝐻π‘₯))β€˜((Idβ€˜πΆ)β€˜π‘₯)) = ((Idβ€˜π·)β€˜(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯)))
9989, 98eqtrd 2772 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) β†’ ((π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))π‘₯)β€˜((Idβ€˜(𝐢 β†Ύcat 𝐻))β€˜π‘₯)) = ((Idβ€˜π·)β€˜(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯)))
10023ad2ant1 1133 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝐻 ∈ (Subcatβ€˜πΆ))
101343ad2ant1 1133 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝐻 Fn (dom dom 𝐻 Γ— dom dom 𝐻))
102 simp21 1206 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
103383ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ dom dom 𝐻 = (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
104102, 103eleqtrrd 2836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ π‘₯ ∈ dom dom 𝐻)
105 eqid 2732 . . . . . . . 8 (compβ€˜πΆ) = (compβ€˜πΆ)
106 simp22 1207 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
107106, 103eleqtrrd 2836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑦 ∈ dom dom 𝐻)
108 simp23 1208 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)))
109108, 103eleqtrrd 2836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑧 ∈ dom dom 𝐻)
110 simp3l 1201 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦))
111713ad2ant1 1133 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝐻 = (Hom β€˜(𝐢 β†Ύcat 𝐻)))
112111oveqd 7422 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (π‘₯𝐻𝑦) = (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦))
113110, 112eleqtrrd 2836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑓 ∈ (π‘₯𝐻𝑦))
114 simp3r 1202 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))
115111oveqd 7422 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (𝑦𝐻𝑧) = (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))
116114, 115eleqtrrd 2836 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑔 ∈ (𝑦𝐻𝑧))
117100, 101, 104, 105, 107, 109, 113, 116subccocl 17791 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧)𝑓) ∈ (π‘₯𝐻𝑧))
118117fvresd 6908 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (((π‘₯(2nd β€˜πΉ)𝑧) β†Ύ (π‘₯𝐻𝑧))β€˜(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧)𝑓)) = ((π‘₯(2nd β€˜πΉ)𝑧)β€˜(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧)𝑓)))
119313ad2ant1 1133 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (1st β€˜πΉ)(𝐢 Func 𝐷)(2nd β€˜πΉ))
120353ad2ant1 1133 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ dom dom 𝐻 βŠ† (Baseβ€˜πΆ))
121120, 104sseldd 3982 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ π‘₯ ∈ (Baseβ€˜πΆ))
122120, 107sseldd 3982 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑦 ∈ (Baseβ€˜πΆ))
123120, 109sseldd 3982 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑧 ∈ (Baseβ€˜πΆ))
124100, 101, 52, 104, 107subcss2 17789 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (π‘₯𝐻𝑦) βŠ† (π‘₯(Hom β€˜πΆ)𝑦))
125124, 113sseldd 3982 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑓 ∈ (π‘₯(Hom β€˜πΆ)𝑦))
126100, 101, 52, 107, 109subcss2 17789 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (𝑦𝐻𝑧) βŠ† (𝑦(Hom β€˜πΆ)𝑧))
127126, 116sseldd 3982 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑧))
12828, 52, 105, 22, 119, 121, 122, 123, 125, 127funcco 17817 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ ((π‘₯(2nd β€˜πΉ)𝑧)β€˜(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧)𝑓)) = (((𝑦(2nd β€˜πΉ)𝑧)β€˜π‘”)(⟨((1st β€˜πΉ)β€˜π‘₯), ((1st β€˜πΉ)β€˜π‘¦)⟩(compβ€˜π·)((1st β€˜πΉ)β€˜π‘§))((π‘₯(2nd β€˜πΉ)𝑦)β€˜π‘“)))
129118, 128eqtrd 2772 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (((π‘₯(2nd β€˜πΉ)𝑧) β†Ύ (π‘₯𝐻𝑧))β€˜(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧)𝑓)) = (((𝑦(2nd β€˜πΉ)𝑧)β€˜π‘”)(⟨((1st β€˜πΉ)β€˜π‘₯), ((1st β€˜πΉ)β€˜π‘¦)⟩(compβ€˜π·)((1st β€˜πΉ)β€˜π‘§))((π‘₯(2nd β€˜πΉ)𝑦)β€˜π‘“)))
13013ad2ant1 1133 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ 𝐹 ∈ (𝐢 Func 𝐷))
131130, 100, 101, 104, 109resf2nd 17841 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑧) = ((π‘₯(2nd β€˜πΉ)𝑧) β†Ύ (π‘₯𝐻𝑧)))
13223, 28, 37, 34, 35, 105rescco 17776 . . . . . . . . . 10 (πœ‘ β†’ (compβ€˜πΆ) = (compβ€˜(𝐢 β†Ύcat 𝐻)))
1331323ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (compβ€˜πΆ) = (compβ€˜(𝐢 β†Ύcat 𝐻)))
134133eqcomd 2738 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (compβ€˜(𝐢 β†Ύcat 𝐻)) = (compβ€˜πΆ))
135134oveqd 7422 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (⟨π‘₯, π‘¦βŸ©(compβ€˜(𝐢 β†Ύcat 𝐻))𝑧) = (⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧))
136135oveqd 7422 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(𝐢 β†Ύcat 𝐻))𝑧)𝑓) = (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧)𝑓))
137131, 136fveq12d 6895 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ ((π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑧)β€˜(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜(𝐢 β†Ύcat 𝐻))𝑧)𝑓)) = (((π‘₯(2nd β€˜πΉ)𝑧) β†Ύ (π‘₯𝐻𝑧))β€˜(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜πΆ)𝑧)𝑓)))
138104fvresd 6908 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯) = ((1st β€˜πΉ)β€˜π‘₯))
139107fvresd 6908 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘¦) = ((1st β€˜πΉ)β€˜π‘¦))
140138, 139opeq12d 4880 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ ⟨(((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘₯), (((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘¦)⟩ = ⟨((1st β€˜πΉ)β€˜π‘₯), ((1st β€˜πΉ)β€˜π‘¦)⟩)
141109fvresd 6908 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (((1st β€˜πΉ) β†Ύ dom dom 𝐻)β€˜π‘§) = ((1st β€˜πΉ)β€˜π‘§))
142140, 141oveq12d 7423 . . . . . 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 β€˜πΉ)β€˜π‘§)))
143130, 100, 101, 107, 109resf2nd 17841 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (𝑦(2nd β€˜(𝐹 β†Ύf 𝐻))𝑧) = ((𝑦(2nd β€˜πΉ)𝑧) β†Ύ (𝑦𝐻𝑧)))
144143fveq1d 6890 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ ((𝑦(2nd β€˜(𝐹 β†Ύf 𝐻))𝑧)β€˜π‘”) = (((𝑦(2nd β€˜πΉ)𝑧) β†Ύ (𝑦𝐻𝑧))β€˜π‘”))
145116fvresd 6908 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (((𝑦(2nd β€˜πΉ)𝑧) β†Ύ (𝑦𝐻𝑧))β€˜π‘”) = ((𝑦(2nd β€˜πΉ)𝑧)β€˜π‘”))
146144, 145eqtrd 2772 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ ((𝑦(2nd β€˜(𝐹 β†Ύf 𝐻))𝑧)β€˜π‘”) = ((𝑦(2nd β€˜πΉ)𝑧)β€˜π‘”))
147130, 100, 101, 104, 107resf2nd 17841 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦) = ((π‘₯(2nd β€˜πΉ)𝑦) β†Ύ (π‘₯𝐻𝑦)))
148147fveq1d 6890 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ ((π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦)β€˜π‘“) = (((π‘₯(2nd β€˜πΉ)𝑦) β†Ύ (π‘₯𝐻𝑦))β€˜π‘“))
149113fvresd 6908 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ (((π‘₯(2nd β€˜πΉ)𝑦) β†Ύ (π‘₯𝐻𝑦))β€˜π‘“) = ((π‘₯(2nd β€˜πΉ)𝑦)β€˜π‘“))
150148, 149eqtrd 2772 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑦 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻)) ∧ 𝑧 ∈ (Baseβ€˜(𝐢 β†Ύcat 𝐻))) ∧ (𝑓 ∈ (π‘₯(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑦) ∧ 𝑔 ∈ (𝑦(Hom β€˜(𝐢 β†Ύcat 𝐻))𝑧))) β†’ ((π‘₯(2nd β€˜(𝐹 β†Ύf 𝐻))𝑦)β€˜π‘“) = ((π‘₯(2nd β€˜πΉ)𝑦)β€˜π‘“))
151142, 146, 150oveq123d 7426 . . . . 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 β€˜πΉ)𝑦)β€˜π‘“)))
152129, 137, 1513eqtr4d 2782 . . . 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 𝐻))𝑦)β€˜π‘“)))
15315, 16, 17, 18, 19, 20, 21, 22, 24, 27, 40, 51, 79, 99, 152isfuncd 17811 . . 3 (πœ‘ β†’ ((1st β€˜πΉ) β†Ύ dom dom 𝐻)((𝐢 β†Ύcat 𝐻) Func 𝐷)(2nd β€˜(𝐹 β†Ύf 𝐻)))
154 df-br 5148 . . 3 (((1st β€˜πΉ) β†Ύ dom dom 𝐻)((𝐢 β†Ύcat 𝐻) Func 𝐷)(2nd β€˜(𝐹 β†Ύf 𝐻)) ↔ ⟨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (2nd β€˜(𝐹 β†Ύf 𝐻))⟩ ∈ ((𝐢 β†Ύcat 𝐻) Func 𝐷))
155153, 154sylib 217 . 2 (πœ‘ β†’ ⟨((1st β€˜πΉ) β†Ύ dom dom 𝐻), (2nd β€˜(𝐹 β†Ύf 𝐻))⟩ ∈ ((𝐢 β†Ύcat 𝐻) Func 𝐷))
15614, 155eqeltrd 2833 1 (πœ‘ β†’ (𝐹 β†Ύf 𝐻) ∈ ((𝐢 β†Ύcat 𝐻) Func 𝐷))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  Vcvv 3474   βŠ† wss 3947  βŸ¨cop 4633   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  dom cdm 5675   β†Ύ cres 5677  Rel wrel 5680   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405  1st c1st 7969  2nd c2nd 7970  Basecbs 17140  Hom chom 17204  compcco 17205  Catccat 17604  Idccid 17605   β†Ύcat cresc 17751  Subcatcsubc 17752   Func cfunc 17800   β†Ύf cresf 17803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-hom 17217  df-cco 17218  df-cat 17608  df-cid 17609  df-homf 17610  df-ssc 17753  df-resc 17754  df-subc 17755  df-func 17804  df-resf 17807
This theorem is referenced by:  funcrngcsetc  46849  funcringcsetc  46886
  Copyright terms: Public domain W3C validator