Theorem gricsym

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

	Ref	Expression
Assertion	gricsym	⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		brgric	⊢ ( 𝐺 ≃𝑔𝑟 𝑆 ↔ ( 𝐺 GraphIso 𝑆 ) ≠ ∅ )
2		n0	⊢ ( ( 𝐺 GraphIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphIso 𝑆 ) )
3	1 2	bitri	⊢ ( 𝐺 ≃𝑔𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphIso 𝑆 ) )
4		grimcnv	⊢ ( 𝐺 ∈ UHGraph → ( 𝑓 ∈ ( 𝐺 GraphIso 𝑆 ) → ◡ 𝑓 ∈ ( 𝑆 GraphIso 𝐺 ) ) )
5		brgrici	⊢ ( ◡ 𝑓 ∈ ( 𝑆 GraphIso 𝐺 ) → 𝑆 ≃𝑔𝑟 𝐺 )
6	4 5	syl6	⊢ ( 𝐺 ∈ UHGraph → ( 𝑓 ∈ ( 𝐺 GraphIso 𝑆 ) → 𝑆 ≃𝑔𝑟 𝐺 ) )
7	6	exlimdv	⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑓 𝑓 ∈ ( 𝐺 GraphIso 𝑆 ) → 𝑆 ≃𝑔𝑟 𝐺 ) )
8	3 7	biimtrid	⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺 ) )