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	$$⊢\left(A\in \mathrm{UHGraph}\wedge B\in \mathrm{UHGraph}\right)\to \left(A{\simeq }_{𝑔𝑟}B\leftrightarrow B{\simeq }_{𝑔𝑟}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		gricsym	$$⊢A\in \mathrm{UHGraph}\to \left(A{\simeq }_{𝑔𝑟}B\to B{\simeq }_{𝑔𝑟}A\right)$$
2		gricsym	$$⊢B\in \mathrm{UHGraph}\to \left(B{\simeq }_{𝑔𝑟}A\to A{\simeq }_{𝑔𝑟}B\right)$$
3	1 2	anbiim	$$⊢\left(A\in \mathrm{UHGraph}\wedge B\in \mathrm{UHGraph}\right)\to \left(A{\simeq }_{𝑔𝑟}B\leftrightarrow B{\simeq }_{𝑔𝑟}A\right)$$