Metamath Proof Explorer

Theorem uvtxnm1nbgr

Description: A universal vertex has n - 1 neighbors in a finite graph with n vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypothesis uvtxnm1nbgr.v 
|- V = ( Vtx ` G )
Assertion uvtxnm1nbgr 
|- ( ( G e. FinUSGraph /\ N e. ( UnivVtx ` G ) ) -> ( # ` ( G NeighbVtx N ) ) = ( ( # ` V ) - 1 ) )

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v 
 |-  V = ( Vtx ` G )
2 1 uvtxnbgr 
 |-  ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
3 2 adantl 
 |-  ( ( G e. FinUSGraph /\ N e. ( UnivVtx ` G ) ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
4 3 fveq2d 
 |-  ( ( G e. FinUSGraph /\ N e. ( UnivVtx ` G ) ) -> ( # ` ( G NeighbVtx N ) ) = ( # ` ( V \ { N } ) ) )
5 1 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> V e. Fin )
6 1 uvtxisvtx 
 |-  ( N e. ( UnivVtx ` G ) -> N e. V )
7 6 snssd 
 |-  ( N e. ( UnivVtx ` G ) -> { N } C_ V )
8 hashssdif 
 |-  ( ( V e. Fin /\ { N } C_ V ) -> ( # ` ( V \ { N } ) ) = ( ( # ` V ) - ( # ` { N } ) ) )
9 5 7 8 syl2an 
 |-  ( ( G e. FinUSGraph /\ N e. ( UnivVtx ` G ) ) -> ( # ` ( V \ { N } ) ) = ( ( # ` V ) - ( # ` { N } ) ) )
10 hashsng 
 |-  ( N e. ( UnivVtx ` G ) -> ( # ` { N } ) = 1 )
11 10 adantl 
 |-  ( ( G e. FinUSGraph /\ N e. ( UnivVtx ` G ) ) -> ( # ` { N } ) = 1 )
12 11 oveq2d 
 |-  ( ( G e. FinUSGraph /\ N e. ( UnivVtx ` G ) ) -> ( ( # ` V ) - ( # ` { N } ) ) = ( ( # ` V ) - 1 ) )
13 4 9 12 3eqtrd 
 |-  ( ( G e. FinUSGraph /\ N e. ( UnivVtx ` G ) ) -> ( # ` ( G NeighbVtx N ) ) = ( ( # ` V ) - 1 ) )