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	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) )
	coffth.g	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
Assertion	coffth	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coffth.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) )
2		coffth.g	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
3	1	elin1d	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
4	2	elin1d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Full 𝐸 ) )
5	3 4	cofull	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) ∈ ( 𝐶 Full 𝐸 ) )
6	1	elin2d	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Faith 𝐷 ) )
7	2	elin2d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Faith 𝐸 ) )
8	6 7	cofth	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) ∈ ( 𝐶 Faith 𝐸 ) )
9	5 8	elind	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )