Metamath Proof Explorer

Theorem nbusgrvtxm1uvtx

Description: If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020) (Proof shortened by AV, 13-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v ⊢ V = Vtx ⁡ G
2 1 nbgrssovtx ⊢ G NeighbVtx U ⊆ V ∖ U
3 2 sseli ⊢ v ∈ G NeighbVtx U → v ∈ V ∖ U
4 eldifsn ⊢ v ∈ V ∖ U ↔ v ∈ V ∧ v ≠ U
5 1 nbusgrvtxm1 ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → v ∈ V ∧ v ≠ U → v ∈ G NeighbVtx U
6 5 imp ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ G NeighbVtx U = V − 1 → v ∈ V ∧ v ≠ U → v ∈ G NeighbVtx U
7 4 6 biimtrid ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ G NeighbVtx U = V − 1 → v ∈ V ∖ U → v ∈ G NeighbVtx U
8 3 7 impbid2 ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ G NeighbVtx U = V − 1 → v ∈ G NeighbVtx U ↔ v ∈ V ∖ U
9 8 eqrdv ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ G NeighbVtx U = V − 1 → G NeighbVtx U = V ∖ U
10 1 uvtxnbgrb ⊢ U ∈ V → U ∈ UnivVtx ⁡ G ↔ G NeighbVtx U = V ∖ U
11 10 ad2antlr ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ G NeighbVtx U = V − 1 → U ∈ UnivVtx ⁡ G ↔ G NeighbVtx U = V ∖ U
12 9 11 mpbird ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ G NeighbVtx U = V − 1 → U ∈ UnivVtx ⁡ G
13 12 ex ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → U ∈ UnivVtx ⁡ G