Metamath Proof Explorer

Theorem rusgr1vtx

Description: If a k-regular simple graph has only one vertex, then k must be 0 . (Contributed by Alexander van der Vekens, 4-Sep-2018) (Revised by AV, 27-Dec-2020)

Ref Expression
Assertion rusgr1vtx 
|- ( ( ( # ` ( Vtx ` G ) ) = 1 /\ G RegUSGraph K ) -> K = 0 )

Proof

Step Hyp Ref Expression
1 nbgr1vtx 
 |-  ( ( # ` ( Vtx ` G ) ) = 1 -> ( G NeighbVtx v ) = (/) )
2 1 ralrimivw 
 |-  ( ( # ` ( Vtx ` G ) ) = 1 -> A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 rusgrpropnb 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K ) )
5 2 4 anim12i 
 |-  ( ( ( # ` ( Vtx ` G ) ) = 1 /\ G RegUSGraph K ) -> ( A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) /\ ( G e. USGraph /\ K e. NN0* /\ A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K ) ) )
6 fvex 
 |-  ( Vtx ` G ) e. _V
7 rusgr1vtxlem 
 |-  ( ( ( A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K /\ A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) ) /\ ( ( Vtx ` G ) e. _V /\ ( # ` ( Vtx ` G ) ) = 1 ) ) -> K = 0 )
8 7 ex 
 |-  ( ( A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K /\ A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) ) -> ( ( ( Vtx ` G ) e. _V /\ ( # ` ( Vtx ` G ) ) = 1 ) -> K = 0 ) )
9 6 8 mpani 
 |-  ( ( A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K /\ A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) ) -> ( ( # ` ( Vtx ` G ) ) = 1 -> K = 0 ) )
10 9 ex 
 |-  ( A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K -> ( A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) -> ( ( # ` ( Vtx ` G ) ) = 1 -> K = 0 ) ) )
11 10 3ad2ant3 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K ) -> ( A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) -> ( ( # ` ( Vtx ` G ) ) = 1 -> K = 0 ) ) )
12 11 com13 
 |-  ( ( # ` ( Vtx ` G ) ) = 1 -> ( A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) -> ( ( G e. USGraph /\ K e. NN0* /\ A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K ) -> K = 0 ) ) )
13 12 impd 
 |-  ( ( # ` ( Vtx ` G ) ) = 1 -> ( ( A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) /\ ( G e. USGraph /\ K e. NN0* /\ A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K ) ) -> K = 0 ) )
14 13 adantr 
 |-  ( ( ( # ` ( Vtx ` G ) ) = 1 /\ G RegUSGraph K ) -> ( ( A. v e. ( Vtx ` G ) ( G NeighbVtx v ) = (/) /\ ( G e. USGraph /\ K e. NN0* /\ A. v e. ( Vtx ` G ) ( # ` ( G NeighbVtx v ) ) = K ) ) -> K = 0 ) )
15 5 14 mpd 
 |-  ( ( ( # ` ( Vtx ` G ) ) = 1 /\ G RegUSGraph K ) -> K = 0 )