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=VtxG
Assertion nbusgrvtxm1 GFinUSGraphUVGNeighbVtxU=V1MVMUMGNeighbVtxU

Proof

Step Hyp Ref Expression
1 hashnbusgrnn0.v V=VtxG
2 ax-1 MGNeighbVtxUMVMUMGNeighbVtxU
3 2 2a1d MGNeighbVtxUGFinUSGraphUVGNeighbVtxU=V1MVMUMGNeighbVtxU
4 simpr ¬MGNeighbVtxUGFinUSGraphUVGFinUSGraphUV
5 4 adantr ¬MGNeighbVtxUGFinUSGraphUVMVMUGFinUSGraphUV
6 simprl ¬MGNeighbVtxUGFinUSGraphUVMVMUMV
7 simpr MVMUMU
8 7 adantl ¬MGNeighbVtxUGFinUSGraphUVMVMUMU
9 df-nel MGNeighbVtxU¬MGNeighbVtxU
10 9 biimpri ¬MGNeighbVtxUMGNeighbVtxU
11 10 adantr ¬MGNeighbVtxUGFinUSGraphUVMGNeighbVtxU
12 11 adantr ¬MGNeighbVtxUGFinUSGraphUVMVMUMGNeighbVtxU
13 1 nbfusgrlevtxm2 GFinUSGraphUVMVMUMGNeighbVtxUGNeighbVtxUV2
14 5 6 8 12 13 syl13anc ¬MGNeighbVtxUGFinUSGraphUVMVMUGNeighbVtxUV2
15 breq1 GNeighbVtxU=V1GNeighbVtxUV2V1V2
16 15 adantl ¬MGNeighbVtxUGFinUSGraphUVMVMUGNeighbVtxU=V1GNeighbVtxUV2V1V2
17 1 fusgrvtxfi GFinUSGraphVFin
18 hashcl VFinV0
19 nn0re V0V
20 1red V1
21 2re 2
22 21 a1i V2
23 id VV
24 1lt2 1<2
25 24 a1i V1<2
26 20 22 23 25 ltsub2dd VV2<V1
27 23 22 resubcld VV2
28 peano2rem VV1
29 27 28 ltnled VV2<V1¬V1V2
30 26 29 mpbid V¬V1V2
31 19 30 syl V0¬V1V2
32 17 18 31 3syl GFinUSGraph¬V1V2
33 32 pm2.21d GFinUSGraphV1V2MGNeighbVtxU
34 33 adantr GFinUSGraphUVV1V2MGNeighbVtxU
35 34 ad3antlr ¬MGNeighbVtxUGFinUSGraphUVMVMUGNeighbVtxU=V1V1V2MGNeighbVtxU
36 16 35 sylbid ¬MGNeighbVtxUGFinUSGraphUVMVMUGNeighbVtxU=V1GNeighbVtxUV2MGNeighbVtxU
37 36 ex ¬MGNeighbVtxUGFinUSGraphUVMVMUGNeighbVtxU=V1GNeighbVtxUV2MGNeighbVtxU
38 14 37 mpid ¬MGNeighbVtxUGFinUSGraphUVMVMUGNeighbVtxU=V1MGNeighbVtxU
39 38 ex ¬MGNeighbVtxUGFinUSGraphUVMVMUGNeighbVtxU=V1MGNeighbVtxU
40 39 com23 ¬MGNeighbVtxUGFinUSGraphUVGNeighbVtxU=V1MVMUMGNeighbVtxU
41 40 ex ¬MGNeighbVtxUGFinUSGraphUVGNeighbVtxU=V1MVMUMGNeighbVtxU
42 3 41 pm2.61i GFinUSGraphUVGNeighbVtxU=V1MVMUMGNeighbVtxU