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 ( 𝐶 Faith 𝐷 )

Proof

Step Hyp Ref Expression
1 fthfunc ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
2 relfunc Rel ( 𝐶 Func 𝐷 )
3 relss ( ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) → ( Rel ( 𝐶 Func 𝐷 ) → Rel ( 𝐶 Faith 𝐷 ) ) )
4 1 2 3 mp2 Rel ( 𝐶 Faith 𝐷 )