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 ~=gr S -> B ~~ C )

Proof

Step Hyp Ref Expression
1 gricen.b 
 |-  B = ( Vtx ` R )
2 gricen.c 
 |-  C = ( Vtx ` S )
3 brgric 
 |-  ( R ~=gr S <-> ( R GraphIso S ) =/= (/) )
4 n0 
 |-  ( ( R GraphIso S ) =/= (/) <-> E. f f e. ( R GraphIso S ) )
5 1 2 grimf1o 
 |-  ( f e. ( R GraphIso S ) -> f : B -1-1-onto-> C )
6 1 fvexi 
 |-  B e. _V
7 6 f1oen 
 |-  ( f : B -1-1-onto-> C -> B ~~ C )
8 5 7 syl 
 |-  ( f e. ( R GraphIso S ) -> B ~~ C )
9 8 exlimiv 
 |-  ( E. f f e. ( R GraphIso S ) -> B ~~ C )
10 4 9 sylbi 
 |-  ( ( R GraphIso S ) =/= (/) -> B ~~ C )
11 3 10 sylbi 
 |-  ( R ~=gr S -> B ~~ C )