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

Metamath Proof Explorer

Theorem grlicen

Description: Locally isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 11-Jun-2025)

Ref Expression
Hypotheses grlicen.b ⊢ B = Vtx ⁡ R
grlicen.c ⊢ C = Vtx ⁡ S
Assertion grlicen ⊢ R ≃ 𝑙𝑔𝑟 S → B ≈ C

Proof

Step Hyp Ref Expression
1 grlicen.b ⊢ B = Vtx ⁡ R
2 grlicen.c ⊢ C = Vtx ⁡ S
3 brgrlic ⊢ R ≃ 𝑙𝑔𝑟 S ↔ R GraphLocIso S ≠ ∅
4 n0 ⊢ R GraphLocIso S ≠ ∅ ↔ ∃ f f ∈ R GraphLocIso S
5 1 2 grlimf1o ⊢ f ∈ R GraphLocIso S → f : B ⟶ 1-1 onto C
6 1 fvexi ⊢ B ∈ V
7 6 f1oen ⊢ f : B ⟶ 1-1 onto C → B ≈ C
8 5 7 syl ⊢ f ∈ R GraphLocIso S → B ≈ C
9 8 exlimiv ⊢ ∃ f f ∈ R GraphLocIso S → B ≈ C
10 4 9 sylbi ⊢ R GraphLocIso S ≠ ∅ → B ≈ C
11 3 10 sylbi ⊢ R ≃ 𝑙𝑔𝑟 S → B ≈ C