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 ⊢ 𝐵 = ( Vtx ‘ 𝑅 )
grlicen.c ⊢ 𝐶 = ( Vtx ‘ 𝑆 )
Assertion grlicen ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶 )

Proof

Step Hyp Ref Expression
1 grlicen.b ⊢ 𝐵 = ( Vtx ‘ 𝑅 )
2 grlicen.c ⊢ 𝐶 = ( Vtx ‘ 𝑆 )
3 brgrlic ⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ )
4 n0 ⊢ ( ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) )
5 1 2 grlimf1o ⊢ ( 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) → 𝑓 : 𝐵 –1-1-onto→ 𝐶 )
6 1 fvexi ⊢ 𝐵 ∈ V
7 6 f1oen ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 → 𝐵 ≈ 𝐶 )
8 5 7 syl ⊢ ( 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) → 𝐵 ≈ 𝐶 )
9 8 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) → 𝐵 ≈ 𝐶 )
10 4 9 sylbi ⊢ ( ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ → 𝐵 ≈ 𝐶 )
11 3 10 sylbi ⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶 )