Metamath Proof Explorer


Theorem ffthres2c

Description: Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses ffthres2c.a A = Base C
ffthres2c.e E = D 𝑠 S
ffthres2c.d φ D Cat
ffthres2c.r φ S V
ffthres2c.1 φ F : A S
Assertion ffthres2c φ F C Full D C Faith D G F C Full E C Faith E G

Proof

Step Hyp Ref Expression
1 ffthres2c.a A = Base C
2 ffthres2c.e E = D 𝑠 S
3 ffthres2c.d φ D Cat
4 ffthres2c.r φ S V
5 ffthres2c.1 φ F : A S
6 1 2 3 4 5 fullres2c φ F C Full D G F C Full E G
7 1 2 3 4 5 fthres2c φ F C Faith D G F C Faith E G
8 6 7 anbi12d φ F C Full D G F C Faith D G F C Full E G F C Faith E G
9 brin F C Full D C Faith D G F C Full D G F C Faith D G
10 brin F C Full E C Faith E G F C Full E G F C Faith E G
11 8 9 10 3bitr4g φ F C Full D C Faith D G F C Full E C Faith E G