Theorem grlicrel

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

	Ref	Expression
Assertion	grlicrel	⊢ Rel ≃𝑙𝑔𝑟

Proof

Step	Hyp	Ref	Expression
1		df-grlic	⊢ ≃𝑙𝑔𝑟 = ( ◡ GraphLocIso “ ( V ∖ 1o ) )
2		cnvimass	⊢ ( ◡ GraphLocIso “ ( V ∖ 1o ) ) ⊆ dom GraphLocIso
3		grlimfn	⊢ GraphLocIso Fn ( V × V )
4	3	fndmi	⊢ dom GraphLocIso = ( V × V )
5	2 4	sseqtri	⊢ ( ◡ GraphLocIso “ ( V ∖ 1o ) ) ⊆ ( V × V )
6	1 5	eqsstri	⊢ ≃𝑙𝑔𝑟 ⊆ ( V × V )
7		relxp	⊢ Rel ( V × V )
8		relss	⊢ ( ≃𝑙𝑔𝑟 ⊆ ( V × V ) → ( Rel ( V × V ) → Rel ≃𝑙𝑔𝑟 ) )
9	6 7 8	mp2	⊢ Rel ≃𝑙𝑔𝑟