Metamath Proof Explorer

Theorem grlicrcl

Description: Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025)

Ref Expression
Assertion grlicrcl ⊢ G ≃ 𝑙𝑔𝑟 S → G ∈ V ∧ S ∈ V

Proof

Step Hyp Ref Expression
1 brgrlic ⊢ G ≃ 𝑙𝑔𝑟 S ↔ G GraphLocIso S ≠ ∅
2 grlimdmrel ⊢ Rel ⁡ dom ⁡ GraphLocIso
3 2 ovprc ⊢ ¬ G ∈ V ∧ S ∈ V → G GraphLocIso S = ∅
4 3 necon1ai ⊢ G GraphLocIso S ≠ ∅ → G ∈ V ∧ S ∈ V
5 1 4 sylbi ⊢ G ≃ 𝑙𝑔𝑟 S → G ∈ V ∧ S ∈ V