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 ⊢ G ∈ UHGraph ∧ H ∈ UHGraph → G ≃ 𝑔𝑟 H → G ≃ 𝑙𝑔𝑟 H

Proof

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