This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fusgrn0degnn0

Description: In a nonempty, finite graph there is a vertex having a nonnegative integer as degree. (Contributed by Alexander van der Vekens, 6-Sep-2018) (Revised by AV, 1-Apr-2021)

Ref Expression
Hypothesis fusgrn0degnn0.v 
|- V = ( Vtx ` G )
Assertion fusgrn0degnn0 
|- ( ( G e. FinUSGraph /\ V =/= (/) ) -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n )

Proof

Step Hyp Ref Expression
1 fusgrn0degnn0.v 
 |-  V = ( Vtx ` G )
2 n0 
 |-  ( V =/= (/) <-> E. k k e. V )
3 1 vtxdgfusgr 
 |-  ( G e. FinUSGraph -> A. u e. V ( ( VtxDeg ` G ) ` u ) e. NN0 )
4 fveq2 
 |-  ( u = k -> ( ( VtxDeg ` G ) ` u ) = ( ( VtxDeg ` G ) ` k ) )
5 4 eleq1d 
 |-  ( u = k -> ( ( ( VtxDeg ` G ) ` u ) e. NN0 <-> ( ( VtxDeg ` G ) ` k ) e. NN0 ) )
6 5 rspcv 
 |-  ( k e. V -> ( A. u e. V ( ( VtxDeg ` G ) ` u ) e. NN0 -> ( ( VtxDeg ` G ) ` k ) e. NN0 ) )
7 risset 
 |-  ( ( ( VtxDeg ` G ) ` k ) e. NN0 <-> E. n e. NN0 n = ( ( VtxDeg ` G ) ` k ) )
8 fveqeq2 
 |-  ( v = k -> ( ( ( VtxDeg ` G ) ` v ) = n <-> ( ( VtxDeg ` G ) ` k ) = n ) )
9 eqcom 
 |-  ( ( ( VtxDeg ` G ) ` k ) = n <-> n = ( ( VtxDeg ` G ) ` k ) )
10 8 9 bitrdi 
 |-  ( v = k -> ( ( ( VtxDeg ` G ) ` v ) = n <-> n = ( ( VtxDeg ` G ) ` k ) ) )
11 10 rexbidv 
 |-  ( v = k -> ( E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n <-> E. n e. NN0 n = ( ( VtxDeg ` G ) ` k ) ) )
12 11 rspcev 
 |-  ( ( k e. V /\ E. n e. NN0 n = ( ( VtxDeg ` G ) ` k ) ) -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n )
13 12 expcom 
 |-  ( E. n e. NN0 n = ( ( VtxDeg ` G ) ` k ) -> ( k e. V -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n ) )
14 7 13 sylbi 
 |-  ( ( ( VtxDeg ` G ) ` k ) e. NN0 -> ( k e. V -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n ) )
15 14 com12 
 |-  ( k e. V -> ( ( ( VtxDeg ` G ) ` k ) e. NN0 -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n ) )
16 6 15 syld 
 |-  ( k e. V -> ( A. u e. V ( ( VtxDeg ` G ) ` u ) e. NN0 -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n ) )
17 3 16 syl5 
 |-  ( k e. V -> ( G e. FinUSGraph -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n ) )
18 17 exlimiv 
 |-  ( E. k k e. V -> ( G e. FinUSGraph -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n ) )
19 2 18 sylbi 
 |-  ( V =/= (/) -> ( G e. FinUSGraph -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n ) )
20 19 impcom 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> E. v e. V E. n e. NN0 ( ( VtxDeg ` G ) ` v ) = n )