Theorem grlicer

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

	Ref	Expression
Assertion	grlicer	⊢ ( ≃𝑙𝑔𝑟 ∩ ( UHGraph × UHGraph ) ) Er UHGraph

Proof

Step	Hyp	Ref	Expression
1		grlicref	⊢ ( 𝑓 ∈ UHGraph → 𝑓 ≃𝑙𝑔𝑟 𝑓 )
2		grlicsym	⊢ ( 𝑓 ∈ UHGraph → ( 𝑓 ≃𝑙𝑔𝑟 𝑔 → 𝑔 ≃𝑙𝑔𝑟 𝑓 ) )
3		grlictr	⊢ ( ( 𝑓 ≃𝑙𝑔𝑟 𝑔 ∧ 𝑔 ≃𝑙𝑔𝑟 ℎ ) → 𝑓 ≃𝑙𝑔𝑟 ℎ )
4	3	a1i	⊢ ( 𝑓 ∈ UHGraph → ( ( 𝑓 ≃𝑙𝑔𝑟 𝑔 ∧ 𝑔 ≃𝑙𝑔𝑟 ℎ ) → 𝑓 ≃𝑙𝑔𝑟 ℎ ) )
5	1 2 4	brinxper	⊢ ( ≃𝑙𝑔𝑟 ∩ ( UHGraph × UHGraph ) ) Er UHGraph