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

Metamath Proof Explorer

Theorem nbusgrvtxm1

Description: If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020)

Ref Expression
Hypothesis hashnbusgrnn0.v 
|- V = ( Vtx ` G )
Assertion nbusgrvtxm1 
|- ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) ) )

Proof

Step Hyp Ref Expression
1 hashnbusgrnn0.v 
 |-  V = ( Vtx ` G )
2 ax-1 
 |-  ( M e. ( G NeighbVtx U ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) )
3 2 2a1d 
 |-  ( M e. ( G NeighbVtx U ) -> ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) ) ) )
4 simpr 
 |-  ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) -> ( G e. FinUSGraph /\ U e. V ) )
5 4 adantr 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> ( G e. FinUSGraph /\ U e. V ) )
6 simprl 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> M e. V )
7 simpr 
 |-  ( ( M e. V /\ M =/= U ) -> M =/= U )
8 7 adantl 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> M =/= U )
9 df-nel 
 |-  ( M e/ ( G NeighbVtx U ) <-> -. M e. ( G NeighbVtx U ) )
10 9 biranri 
 |-  ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) -> M e/ ( G NeighbVtx U ) )
11 10 adantr 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> M e/ ( G NeighbVtx U ) )
12 1 nbfusgrlevtxm2 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( M e. V /\ M =/= U /\ M e/ ( G NeighbVtx U ) ) ) -> ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) )
13 5 6 8 11 12 syl13anc 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) )
14 breq1 
 |-  ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) <-> ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) ) )
15 14 adantl 
 |-  ( ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) <-> ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) ) )
16 1 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> V e. Fin )
17 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
18 nn0re 
 |-  ( ( # ` V ) e. NN0 -> ( # ` V ) e. RR )
19 1red 
 |-  ( ( # ` V ) e. RR -> 1 e. RR )
20 2re 
 |-  2 e. RR
21 20 a1i 
 |-  ( ( # ` V ) e. RR -> 2 e. RR )
22 id 
 |-  ( ( # ` V ) e. RR -> ( # ` V ) e. RR )
23 1lt2 
 |-  1 < 2
24 23 a1i 
 |-  ( ( # ` V ) e. RR -> 1 < 2 )
25 19 21 22 24 ltsub2dd 
 |-  ( ( # ` V ) e. RR -> ( ( # ` V ) - 2 ) < ( ( # ` V ) - 1 ) )
26 22 21 resubcld 
 |-  ( ( # ` V ) e. RR -> ( ( # ` V ) - 2 ) e. RR )
27 peano2rem 
 |-  ( ( # ` V ) e. RR -> ( ( # ` V ) - 1 ) e. RR )
28 26 27 ltnled 
 |-  ( ( # ` V ) e. RR -> ( ( ( # ` V ) - 2 ) < ( ( # ` V ) - 1 ) <-> -. ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) ) )
29 25 28 mpbid 
 |-  ( ( # ` V ) e. RR -> -. ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) )
30 16 17 18 29 4syl 
 |-  ( G e. FinUSGraph -> -. ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) )
31 30 pm2.21d 
 |-  ( G e. FinUSGraph -> ( ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) -> M e. ( G NeighbVtx U ) ) )
32 31 adantr 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) -> M e. ( G NeighbVtx U ) ) )
33 32 ad3antlr 
 |-  ( ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) -> M e. ( G NeighbVtx U ) ) )
34 15 33 sylbid 
 |-  ( ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) -> M e. ( G NeighbVtx U ) ) )
35 34 ex 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) -> M e. ( G NeighbVtx U ) ) ) )
36 13 35 mpid 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> M e. ( G NeighbVtx U ) ) )
37 36 ex 
 |-  ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) -> ( ( M e. V /\ M =/= U ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> M e. ( G NeighbVtx U ) ) ) )
38 37 com23 
 |-  ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) ) )
39 38 ex 
 |-  ( -. M e. ( G NeighbVtx U ) -> ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) ) ) )
40 3 39 pm2.61i 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) ) )