Theorem gricsymb

Description: Graph isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 11-Nov-2022) (Proof shortened by AV, 3-May-2025)

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

Proof

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