This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coffth

Description: The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses coffth.f 
|- ( ph -> F e. ( ( C Full D ) i^i ( C Faith D ) ) )
coffth.g 
|- ( ph -> G e. ( ( D Full E ) i^i ( D Faith E ) ) )
Assertion coffth 
|- ( ph -> ( G o.func F ) e. ( ( C Full E ) i^i ( C Faith E ) ) )

Proof

Step Hyp Ref Expression
1 coffth.f 
 |-  ( ph -> F e. ( ( C Full D ) i^i ( C Faith D ) ) )
2 coffth.g 
 |-  ( ph -> G e. ( ( D Full E ) i^i ( D Faith E ) ) )
3 1 elin1d 
 |-  ( ph -> F e. ( C Full D ) )
4 2 elin1d 
 |-  ( ph -> G e. ( D Full E ) )
5 3 4 cofull 
 |-  ( ph -> ( G o.func F ) e. ( C Full E ) )
6 1 elin2d 
 |-  ( ph -> F e. ( C Faith D ) )
7 2 elin2d 
 |-  ( ph -> G e. ( D Faith E ) )
8 6 7 cofth 
 |-  ( ph -> ( G o.func F ) e. ( C Faith E ) )
9 5 8 elind 
 |-  ( ph -> ( G o.func F ) e. ( ( C Full E ) i^i ( C Faith E ) ) )