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

Metamath Proof Explorer

Theorem uvtxnbgrvtx

Description: A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 30-Oct-2020)

Ref Expression
Hypothesis uvtxel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion uvtxnbgrvtx ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) )

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 vtxnbuvtx ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) )
3 eleq1w ⊢ ( 𝑛 = 𝑣 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ↔ 𝑣 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) )
4 3 rspcva ⊢ ( ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → 𝑣 ∈ ( 𝐺 NeighbVtx 𝑁 ) )
5 nbgrsym ⊢ ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑁 ) ↔ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) )
6 5 a1i ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑁 ) ↔ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
7 4 6 syl5ibcom ⊢ ( ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
8 7 expcom ⊢ ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) )
9 8 com23 ⊢ ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) )
10 2 9 mpcom ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
11 10 ralrimiv ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑁 ∈ ( 𝐺 NeighbVtx 𝑣 ) )