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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion nbusgrvtxm1uvtx ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 1 nbgrssovtx ( 𝐺 NeighbVtx 𝑈 ) ⊆ ( 𝑉 ∖ { 𝑈 } )
3 2 sseli ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) → 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) )
4 eldifsn ( 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) ↔ ( 𝑣𝑉𝑣𝑈 ) )
5 1 nbusgrvtxm1 ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( ( 𝑣𝑉𝑣𝑈 ) → 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) ) )
6 5 imp ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( ( 𝑣𝑉𝑣𝑈 ) → 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) )
7 4 6 syl5bi ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) → 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) )
8 3 7 impbid2 ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) ) )
9 8 eqrdv ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝐺 NeighbVtx 𝑈 ) = ( 𝑉 ∖ { 𝑈 } ) )
10 1 uvtxnbgrb ( 𝑈𝑉 → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝐺 NeighbVtx 𝑈 ) = ( 𝑉 ∖ { 𝑈 } ) ) )
11 10 ad2antlr ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝐺 NeighbVtx 𝑈 ) = ( 𝑉 ∖ { 𝑈 } ) ) )
12 9 11 mpbird ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) )
13 12 ex ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ) )