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 )