Metamath Proof Explorer

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 ⊢ f ∈ UHGraph → f ≃ 𝑙𝑔𝑟 f
2 grlicsym ⊢ f ∈ UHGraph → f ≃ 𝑙𝑔𝑟 g → g ≃ 𝑙𝑔𝑟 f
3 grlictr ⊢ f ≃ 𝑙𝑔𝑟 g ∧ g ≃ 𝑙𝑔𝑟 h → f ≃ 𝑙𝑔𝑟 h
4 3 a1i ⊢ f ∈ UHGraph → f ≃ 𝑙𝑔𝑟 g ∧ g ≃ 𝑙𝑔𝑟 h → f ≃ 𝑙𝑔𝑟 h
5 1 2 4 brinxper ⊢ ≃ 𝑙𝑔𝑟 ∩ UHGraph × UHGraph Er UHGraph