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 )

Proof

Step Hyp Ref Expression
1 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
2 relfunc 
 |-  Rel ( C Func D )
3 relss 
 |-  ( ( C Full D ) C_ ( C Func D ) -> ( Rel ( C Func D ) -> Rel ( C Full D ) ) )
4 1 2 3 mp2 
 |-  Rel ( C Full D )