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 ~=lgr

Proof

Step	Hyp	Ref	Expression
1		df-grlic	|- ~=lgr = ( `' GraphLocIso " ( _V \ 1o ) )
2		cnvimass	|- ( `' GraphLocIso " ( _V \ 1o ) ) C_ dom GraphLocIso
3		grlimfn	|- GraphLocIso Fn ( _V X. _V )
4	3	fndmi	|- dom GraphLocIso = ( _V X. _V )
5	2 4	sseqtri	|- ( `' GraphLocIso " ( _V \ 1o ) ) C_ ( _V X. _V )
6	1 5	eqsstri	|- ~=lgr C_ ( _V X. _V )
7		relxp	|- Rel ( _V X. _V )
8		relss	|- ( ~=lgr C_ ( _V X. _V ) -> ( Rel ( _V X. _V ) -> Rel ~=lgr ) )
9	6 7 8	mp2	|- Rel ~=lgr