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 Func D
2 relfunc Rel C Func D
3 relss C Faith D C Func D Rel C Func D Rel C Faith D
4 1 2 3 mp2 Rel C Faith D