Metamath Proof Explorer

Theorem grlicsymb

Description: Graph local isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 9-Jun-2025)

Ref Expression
Assertion grlicsymb ⊢ A ∈ UHGraph ∧ B ∈ UHGraph → A ≃ 𝑙𝑔𝑟 B ↔ B ≃ 𝑙𝑔𝑟 A

Proof

Step Hyp Ref Expression
1 grlicsym ⊢ A ∈ UHGraph → A ≃ 𝑙𝑔𝑟 B → B ≃ 𝑙𝑔𝑟 A
2 grlicsym ⊢ B ∈ UHGraph → B ≃ 𝑙𝑔𝑟 A → A ≃ 𝑙𝑔𝑟 B
3 1 2 anbiim ⊢ A ∈ UHGraph ∧ B ∈ UHGraph → A ≃ 𝑙𝑔𝑟 B ↔ B ≃ 𝑙𝑔𝑟 A