gricsym

Description: Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 3-May-2025)

		Ref	Expression
	Assertion	gricsym	$⊢ G \in UHGraph \to (G ≃_{𝑔𝑟} S \to S ≃_{𝑔𝑟} G)$

Step	Hyp	Ref	Expression
1		brgric	$⊢ G ≃_{𝑔𝑟} S \leftrightarrow G GraphIso S \neq \emptyset$
2		n0	$⊢ G GraphIso S \neq \emptyset \leftrightarrow \exists f f \in (G GraphIso S)$
3	1 2	bitri	$⊢ G ≃_{𝑔𝑟} S \leftrightarrow \exists f f \in (G GraphIso S)$
4		grimcnv	$⊢ G \in UHGraph \to (f \in (G GraphIso S) \to f^{-1} \in (S GraphIso G))$
5		brgrici	$⊢ f^{-1} \in (S GraphIso G) \to S ≃_{𝑔𝑟} G$
6	4 5	syl6	$⊢ G \in UHGraph \to (f \in (G GraphIso S) \to S ≃_{𝑔𝑟} G)$
7	6	exlimdv	$⊢ G \in UHGraph \to (\exists f f \in (G GraphIso S) \to S ≃_{𝑔𝑟} G)$
8	3 7	biimtrid	$⊢ G \in UHGraph \to (G ≃_{𝑔𝑟} S \to S ≃_{𝑔𝑟} G)$

Metamath Proof Explorer