This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ( 𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺 ) )