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 biimpri 
 |-  ( -. M e. ( G NeighbVtx U ) -> M e/ ( G NeighbVtx U ) )
11 10 adantr 
 |-  ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) -> M e/ ( G NeighbVtx U ) )
12 11 adantr 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> M e/ ( G NeighbVtx U ) )
13 1 nbfusgrlevtxm2 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( M e. V /\ M =/= U /\ M e/ ( G NeighbVtx U ) ) ) -> ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) )
14 5 6 8 12 13 syl13anc 
 |-  ( ( ( -. M e. ( G NeighbVtx U ) /\ ( G e. FinUSGraph /\ U e. V ) ) /\ ( M e. V /\ M =/= U ) ) -> ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) )
15 breq1 
 |-  ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( # ` ( G NeighbVtx U ) ) <_ ( ( # ` V ) - 2 ) <-> ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) ) )
16 15 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 ) ) )
17 1 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> V e. Fin )
18 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
19 nn0re 
 |-  ( ( # ` V ) e. NN0 -> ( # ` V ) e. RR )
20 1red 
 |-  ( ( # ` V ) e. RR -> 1 e. RR )
21 2re 
 |-  2 e. RR
22 21 a1i 
 |-  ( ( # ` V ) e. RR -> 2 e. RR )
23 id 
 |-  ( ( # ` V ) e. RR -> ( # ` V ) e. RR )
24 1lt2 
 |-  1 < 2
25 24 a1i 
 |-  ( ( # ` V ) e. RR -> 1 < 2 )
26 20 22 23 25 ltsub2dd 
 |-  ( ( # ` V ) e. RR -> ( ( # ` V ) - 2 ) < ( ( # ` V ) - 1 ) )
27 23 22 resubcld 
 |-  ( ( # ` V ) e. RR -> ( ( # ` V ) - 2 ) e. RR )
28 peano2rem 
 |-  ( ( # ` V ) e. RR -> ( ( # ` V ) - 1 ) e. RR )
29 27 28 ltnled 
 |-  ( ( # ` V ) e. RR -> ( ( ( # ` V ) - 2 ) < ( ( # ` V ) - 1 ) <-> -. ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) ) )
30 26 29 mpbid 
 |-  ( ( # ` V ) e. RR -> -. ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) )
31 19 30 syl 
 |-  ( ( # ` V ) e. NN0 -> -. ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) )
32 17 18 31 3syl 
 |-  ( G e. FinUSGraph -> -. ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) )
33 32 pm2.21d 
 |-  ( G e. FinUSGraph -> ( ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) -> M e. ( G NeighbVtx U ) ) )
34 33 adantr 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( ( # ` V ) - 1 ) <_ ( ( # ` V ) - 2 ) -> M e. ( G NeighbVtx U ) ) )
35 34 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 ) ) )
36 16 35 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 ) ) )
37 36 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 ) ) ) )
38 14 37 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 ) ) )
39 38 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 ) ) ) )
40 39 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 ) ) ) )
41 40 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 ) ) ) ) )
42 3 41 pm2.61i 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( M e. V /\ M =/= U ) -> M e. ( G NeighbVtx U ) ) ) )