Metamath Proof Explorer

Theorem uvtxnm1nbgr

Description: A universal vertex has n - 1 neighbors in a finite graph with n vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypothesis uvtxnm1nbgr.v ⊢ V = Vtx ⁡ G
Assertion uvtxnm1nbgr ⊢ G ∈ FinUSGraph ∧ N ∈ UnivVtx ⁡ G → G NeighbVtx N = V − 1

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v ⊢ V = Vtx ⁡ G
2 1 uvtxnbgr ⊢ N ∈ UnivVtx ⁡ G → G NeighbVtx N = V ∖ N
3 2 adantl ⊢ G ∈ FinUSGraph ∧ N ∈ UnivVtx ⁡ G → G NeighbVtx N = V ∖ N
4 3 fveq2d ⊢ G ∈ FinUSGraph ∧ N ∈ UnivVtx ⁡ G → G NeighbVtx N = V ∖ N
5 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → V ∈ Fin
6 1 uvtxisvtx ⊢ N ∈ UnivVtx ⁡ G → N ∈ V
7 6 snssd ⊢ N ∈ UnivVtx ⁡ G → N ⊆ V
8 hashssdif ⊢ V ∈ Fin ∧ N ⊆ V → V ∖ N = V − N
9 5 7 8 syl2an ⊢ G ∈ FinUSGraph ∧ N ∈ UnivVtx ⁡ G → V ∖ N = V − N
10 hashsng ⊢ N ∈ UnivVtx ⁡ G → N = 1
11 10 adantl ⊢ G ∈ FinUSGraph ∧ N ∈ UnivVtx ⁡ G → N = 1
12 11 oveq2d ⊢ G ∈ FinUSGraph ∧ N ∈ UnivVtx ⁡ G → V − N = V − 1
13 4 9 12 3eqtrd ⊢ G ∈ FinUSGraph ∧ N ∈ UnivVtx ⁡ G → G NeighbVtx N = V − 1