This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 uvtxnbgr ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑉 ∖ { 𝑁 } ) )
3 2 adantl ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑉 ∖ { 𝑁 } ) )
4 3 fveq2d ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑁 ) ) = ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) )
5 1 fusgrvtxfi ⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )
6 1 uvtxisvtx ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑁 ∈ 𝑉 )
7 6 snssd ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → { 𝑁 } ⊆ 𝑉 )
8 hashssdif ⊢ ( ( 𝑉 ∈ Fin ∧ { 𝑁 } ⊆ 𝑉 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − ( ♯ ‘ { 𝑁 } ) ) )
9 5 7 8 syl2an ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − ( ♯ ‘ { 𝑁 } ) ) )
10 hashsng ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( ♯ ‘ { 𝑁 } ) = 1 )
11 10 adantl ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) → ( ♯ ‘ { 𝑁 } ) = 1 )
12 11 oveq2d ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑉 ) − ( ♯ ‘ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
13 4 9 12 3eqtrd ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑁 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )