This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sscrel

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

		Ref	Expression
	Assertion	sscrel	$⊢ Rel \subseteq_{cat}$

Step	Hyp	Ref	Expression
1		df-ssc	$⊢ \subseteq_{cat} = \{⟨h, j⟩ \| \exists t (j Fn (t \times t) \land \exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 j (x))\}$
2	1	relopabiv	$⊢ Rel \subseteq_{cat}$