coffth

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

	Ref	Expression
Hypotheses	coffth.f	$⊢ φ \to F \in ((C Full D) \cap (C Faith D))$
	coffth.g	$⊢ φ \to G \in ((D Full E) \cap (D Faith E))$
Assertion	coffth	$⊢ φ \to G \circ_{func} F \in ((C Full E) \cap (C Faith E))$

Step	Hyp	Ref	Expression
1		coffth.f	$⊢ φ \to F \in ((C Full D) \cap (C Faith D))$
2		coffth.g	$⊢ φ \to G \in ((D Full E) \cap (D Faith E))$
3	1	elin1d	$⊢ φ \to F \in (C Full D)$
4	2	elin1d	$⊢ φ \to G \in (D Full E)$
5	3 4	cofull	$⊢ φ \to G \circ_{func} F \in (C Full E)$
6	1	elin2d	$⊢ φ \to F \in (C Faith D)$
7	2	elin2d	$⊢ φ \to G \in (D Faith E)$
8	6 7	cofth	$⊢ φ \to G \circ_{func} F \in (C Faith E)$
9	5 8	elind	$⊢ φ \to G \circ_{func} F \in ((C Full E) \cap (C Faith E))$

Metamath Proof Explorer