Theorem relfull

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

	Ref	Expression
Assertion	relfull	$$⊢\mathrm{Rel}\left(C\mathrm{Full}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		fullfunc	$$⊢C\mathrm{Full}D\subseteq C\mathrm{Func}D$$
2		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
3		relss	$$⊢C\mathrm{Full}D\subseteq C\mathrm{Func}D\to \left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\to \mathrm{Rel}\left(C\mathrm{Full}D\right)\right)$$
4	1 2 3	mp2	$$⊢\mathrm{Rel}\left(C\mathrm{Full}D\right)$$