gricrel

Description: The "is isomorphic to" relation for graphs is a relation. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)

		Ref	Expression
	Assertion	gricrel	$⊢ Rel ≃_{𝑔𝑟}$

Step	Hyp	Ref	Expression
1		df-gric	$⊢ ≃_{𝑔𝑟} = {GraphIso}^{-1} [V ∖ 1_{𝑜}]$
2		cnvimass	$⊢ {GraphIso}^{-1} [V ∖ 1_{𝑜}] \subseteq dom GraphIso$
3		grimfn	$⊢ GraphIso Fn (V \times V)$
4	3	fndmi	$⊢ dom GraphIso = V \times V$
5	2 4	sseqtri	$⊢ {GraphIso}^{-1} [V ∖ 1_{𝑜}] \subseteq V \times V$
6	1 5	eqsstri	$⊢ ≃_{𝑔𝑟} \subseteq V \times V$
7		relxp	$⊢ Rel (V \times V)$
8		relss	$⊢ ≃_{𝑔𝑟} \subseteq V \times V \to (Rel (V \times V) \to Rel ≃_{𝑔𝑟})$
9	6 7 8	mp2	$⊢ Rel ≃_{𝑔𝑟}$

Metamath Proof Explorer