Theorem relfth

Description: The set of faithful functors is a relation. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Assertion	relfth	⊢ Rel ( 𝐶 Faith 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fthfunc	⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
2		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
3		relss	⊢ ( ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) → ( Rel ( 𝐶 Func 𝐷 ) → Rel ( 𝐶 Faith 𝐷 ) ) )
4	1 2 3	mp2	⊢ Rel ( 𝐶 Faith 𝐷 )