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 ) ) )