Theorem sscrel

Description: The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Assertion	sscrel	⊢ Rel ⊆cat

Proof

Step	Hyp	Ref	Expression
1		df-ssc	⊢ ⊆cat = { ⟨ ℎ , 𝑗 ⟩ ∣ ∃ 𝑡 ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ) }
2	1	relopabiv	⊢ Rel ⊆cat