Theorem grlicer

Description: Local isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 11-Jun-2025)

	Ref	Expression
Assertion	grlicer	|- ( ~=lgr i^i ( UHGraph X. UHGraph ) ) Er UHGraph

Proof

Step	Hyp	Ref	Expression
1		grlicref	|- ( f e. UHGraph -> f ~=lgr f )
2		grlicsym	|- ( f e. UHGraph -> ( f ~=lgr g -> g ~=lgr f ) )
3		grlictr	|- ( ( f ~=lgr g /\ g ~=lgr h ) -> f ~=lgr h )
4	3	a1i	|- ( f e. UHGraph -> ( ( f ~=lgr g /\ g ~=lgr h ) -> f ~=lgr h ) )
5	1 2 4	brinxper	|- ( ~=lgr i^i ( UHGraph X. UHGraph ) ) Er UHGraph