grlicrel

Description: The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025)

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

Step	Hyp	Ref	Expression
1		df-grlic	$⊢ ≃_{𝑙𝑔𝑟} = {GraphLocIso}^{-1} [V ∖ 1_{𝑜}]$
2		cnvimass	$⊢ {GraphLocIso}^{-1} [V ∖ 1_{𝑜}] \subseteq dom GraphLocIso$
3		grlimfn	$⊢ GraphLocIso Fn (V \times V)$
4	3	fndmi	$⊢ dom GraphLocIso = V \times V$
5	2 4	sseqtri	$⊢ {GraphLocIso}^{-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