Metamath Proof Explorer

Theorem gricgrlic

Description: Isomorphic hypergraphs are locally isomorphic. (Contributed by AV, 12-Jun-2025) (Proof shortened by AV, 11-Jul-2025)

Ref Expression
Assertion gricgrlic ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐺 ≃𝑔𝑟 𝐻 → 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )

Proof

Step Hyp Ref Expression
1 brgric ⊢ ( 𝐺 ≃𝑔𝑟 𝐻 ↔ ( 𝐺 GraphIso 𝐻 ) ≠ ∅ )
2 n0 ⊢ ( ( 𝐺 GraphIso 𝐻 ) ≠ ∅ ↔ ∃ 𝑖 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) )
3 uhgrimgrlim ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝑖 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
4 brgrilci ⊢ ( 𝑖 ∈ ( 𝐺 GraphLocIso 𝐻 ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 )
5 3 4 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 )
6 5 3expa ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 )
7 6 expcom ⊢ ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
8 7 exlimiv ⊢ ( ∃ 𝑖 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
9 2 8 sylbi ⊢ ( ( 𝐺 GraphIso 𝐻 ) ≠ ∅ → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
10 1 9 sylbi ⊢ ( 𝐺 ≃𝑔𝑟 𝐻 → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
11 10 com12 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐺 ≃𝑔𝑟 𝐻 → 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )