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

Metamath Proof Explorer

Theorem gricen

Description: Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025)

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

Proof

Step Hyp Ref Expression
1 gricen.b ⊢ B = Vtx ⁡ R
2 gricen.c ⊢ C = Vtx ⁡ S
3 brgric ⊢ R ≃ 𝑔𝑟 S ↔ R GraphIso S ≠ ∅
4 n0 ⊢ R GraphIso S ≠ ∅ ↔ ∃ f f ∈ R GraphIso S
5 1 2 grimf1o ⊢ f ∈ R GraphIso 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 GraphIso S → B ≈ C
9 8 exlimiv ⊢ ∃ f f ∈ R GraphIso S → B ≈ C
10 4 9 sylbi ⊢ R GraphIso S ≠ ∅ → B ≈ C
11 3 10 sylbi ⊢ R ≃ 𝑔𝑟 S → B ≈ C