Theorem grlicrcl

Description: Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025)

	Ref	Expression
Assertion	grlicrcl	|- ( G ~=lgr S -> ( G e. _V /\ S e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		brgrlic	|- ( G ~=lgr S <-> ( G GraphLocIso S ) =/= (/) )
2		grlimdmrel	|- Rel dom GraphLocIso
3	2	ovprc	|- ( -. ( G e. _V /\ S e. _V ) -> ( G GraphLocIso S ) = (/) )
4	3	necon1ai	|- ( ( G GraphLocIso S ) =/= (/) -> ( G e. _V /\ S e. _V ) )
5	1 4	sylbi	|- ( G ~=lgr S -> ( G e. _V /\ S e. _V ) )