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 )

Proof

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