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 ‘ 𝐺 ) ) )