Theorem relfull

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

	Ref	Expression
Assertion	relfull	⊢ Rel ( 𝐶 Full 𝐷 )

Proof

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