Theorem grlicsymb

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

	Ref	Expression
Assertion	grlicsymb	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ) → ( 𝐴 ≃𝑙𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑙𝑔𝑟 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		grlicsym	⊢ ( 𝐴 ∈ UHGraph → ( 𝐴 ≃𝑙𝑔𝑟 𝐵 → 𝐵 ≃𝑙𝑔𝑟 𝐴 ) )
2		grlicsym	⊢ ( 𝐵 ∈ UHGraph → ( 𝐵 ≃𝑙𝑔𝑟 𝐴 → 𝐴 ≃𝑙𝑔𝑟 𝐵 ) )
3	1 2	anbiim	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ) → ( 𝐴 ≃𝑙𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑙𝑔𝑟 𝐴 ) )