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

Proof

Step Hyp Ref Expression
1 grlicen.b 
 |-  B = ( Vtx ` R )
2 grlicen.c 
 |-  C = ( Vtx ` S )
3 brgrlic 
 |-  ( R ~=lgr S <-> ( R GraphLocIso S ) =/= (/) )
4 n0 
 |-  ( ( R GraphLocIso S ) =/= (/) <-> E. f f e. ( R GraphLocIso S ) )
5 1 2 grlimf1o 
 |-  ( f e. ( R GraphLocIso 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 GraphLocIso S ) -> B ~~ C )
9 8 exlimiv 
 |-  ( E. f f e. ( R GraphLocIso S ) -> B ~~ C )
10 4 9 sylbi 
 |-  ( ( R GraphLocIso S ) =/= (/) -> B ~~ C )
11 3 10 sylbi 
 |-  ( R ~=lgr S -> B ~~ C )