Metamath Proof Explorer

Theorem uvtxnbvtxm1

Description: A universal vertex has n - 1 neighbors in a finite simple graph with n vertices. A biconditional version of nbusgrvtxm1uvtx resp. uvtxnm1nbgr . (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v 
 |-  V = ( Vtx ` G )
2 1 uvtxnm1nbgr 
 |-  ( ( G e. FinUSGraph /\ U e. ( UnivVtx ` G ) ) -> ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) )
3 2 ex 
 |-  ( G e. FinUSGraph -> ( U e. ( UnivVtx ` G ) -> ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) )
4 3 adantr 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( U e. ( UnivVtx ` G ) -> ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) )
5 1 nbusgrvtxm1uvtx 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> U e. ( UnivVtx ` G ) ) )
6 4 5 impbid 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( U e. ( UnivVtx ` G ) <-> ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) )