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 ) ) ) |