Metamath Proof Explorer

Theorem fullfunc

Description: A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Assertion fullfunc ⊢CFullD⊆CFuncD

Proof

Step Hyp Ref Expression
1 oveq1 ⊢c=C→cFulld=CFulld
2 oveq1 ⊢c=C→cFuncd=CFuncd
3 1 2 sseq12d ⊢c=C→cFulld⊆cFuncd↔CFulld⊆CFuncd
4 oveq2 ⊢d=D→CFulld=CFullD
5 oveq2 ⊢d=D→CFuncd=CFuncD
6 4 5 sseq12d ⊢d=D→CFulld⊆CFuncd↔CFullD⊆CFuncD
7 ovex ⊢cFuncd∈V
8 simpl ⊢fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y→fcFuncdg
9 8 ssopab2i ⊢fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y⊆fg|fcFuncdg
10 opabss ⊢fg|fcFuncdg⊆cFuncd
11 9 10 sstri ⊢fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y⊆cFuncd
12 7 11 ssexi ⊢fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y∈V
13 df-full ⊢Full=c∈Cat,d∈Cat⟼fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y
14 13 ovmpt4g ⊢c∈Cat∧d∈Cat∧fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y∈V→cFulld=fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y
15 12 14 mp3an3 ⊢c∈Cat∧d∈Cat→cFulld=fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y
16 15 11 eqsstrdi ⊢c∈Cat∧d∈Cat→cFulld⊆cFuncd
17 3 6 16 vtocl2ga ⊢C∈Cat∧D∈Cat→CFullD⊆CFuncD
18 13 mpondm0 ⊢¬C∈Cat∧D∈Cat→CFullD=∅
19 0ss ⊢∅⊆CFuncD
20 18 19 eqsstrdi ⊢¬C∈Cat∧D∈Cat→CFullD⊆CFuncD
21 17 20 pm2.61i ⊢CFullD⊆CFuncD