This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relfull

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

		Ref	Expression
	Assertion	relfull	$⊢ Rel (C Full D)$

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