Metamath Proof Explorer


Theorem fthfunc

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

Ref Expression
Assertion fthfunc C Faith D C Func D

Proof

Step Hyp Ref Expression
1 oveq1 c = C c Faith d = C Faith d
2 oveq1 c = C c Func d = C Func d
3 1 2 sseq12d c = C c Faith d c Func d C Faith d C Func d
4 oveq2 d = D C Faith d = C Faith D
5 oveq2 d = D C Func d = C Func D
6 4 5 sseq12d d = D C Faith d C Func d C Faith D C Func D
7 ovex c Func d V
8 simpl f c Func d g x Base c y Base c Fun x g y -1 f c Func d g
9 8 ssopab2i f g | f c Func d g x Base c y Base c Fun x g y -1 f g | f c Func d g
10 opabss f g | f c Func d g c Func d
11 9 10 sstri f g | f c Func d g x Base c y Base c Fun x g y -1 c Func d
12 7 11 ssexi f g | f c Func d g x Base c y Base c Fun x g y -1 V
13 df-fth Faith = c Cat , d Cat f g | f c Func d g x Base c y Base c Fun x g y -1
14 13 ovmpt4g c Cat d Cat f g | f c Func d g x Base c y Base c Fun x g y -1 V c Faith d = f g | f c Func d g x Base c y Base c Fun x g y -1
15 12 14 mp3an3 c Cat d Cat c Faith d = f g | f c Func d g x Base c y Base c Fun x g y -1
16 15 11 eqsstrdi c Cat d Cat c Faith d c Func d
17 3 6 16 vtocl2ga C Cat D Cat C Faith D C Func D
18 13 mpondm0 ¬ C Cat D Cat C Faith D =
19 0ss C Func D
20 18 19 eqsstrdi ¬ C Cat D Cat C Faith D C Func D
21 17 20 pm2.61i C Faith D C Func D