Metamath Proof Explorer

Theorem fthfunc

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

Ref Expression
Assertion fthfunc ⊢CFaithD⊆CFuncD

Proof

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