Metamath Proof Explorer

Theorem relfth

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

		Ref	Expression
	Assertion	relfth	$⊢ Rel (C Faith D)$

Step	Hyp	Ref	Expression
1		fthfunc	$⊢ C Faith D \subseteq C Func D$
2		relfunc	$⊢ Rel (C Func D)$
3		relss	$⊢ C Faith D \subseteq C Func D \to (Rel (C Func D) \to Rel (C Faith D))$
4	1 2 3	mp2	$⊢ Rel (C Faith D)$