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 ⊢ V = Vtx ⁡ G
Assertion uvtxnbgrvtx ⊢ N ∈ UnivVtx ⁡ G → ∀ v ∈ V ∖ N N ∈ G NeighbVtx v

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 1 vtxnbuvtx ⊢ N ∈ UnivVtx ⁡ G → ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
3 eleq1w ⊢ n = v → n ∈ G NeighbVtx N ↔ v ∈ G NeighbVtx N
4 3 rspcva ⊢ v ∈ V ∖ N ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N → v ∈ G NeighbVtx N
5 nbgrsym ⊢ v ∈ G NeighbVtx N ↔ N ∈ G NeighbVtx v
6 5 a1i ⊢ N ∈ UnivVtx ⁡ G → v ∈ G NeighbVtx N ↔ N ∈ G NeighbVtx v
7 4 6 syl5ibcom ⊢ v ∈ V ∖ N ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N → N ∈ UnivVtx ⁡ G → N ∈ G NeighbVtx v
8 7 expcom ⊢ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N → v ∈ V ∖ N → N ∈ UnivVtx ⁡ G → N ∈ G NeighbVtx v
9 8 com23 ⊢ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N → N ∈ UnivVtx ⁡ G → v ∈ V ∖ N → N ∈ G NeighbVtx v
10 2 9 mpcom ⊢ N ∈ UnivVtx ⁡ G → v ∈ V ∖ N → N ∈ G NeighbVtx v
11 10 ralrimiv ⊢ N ∈ UnivVtx ⁡ G → ∀ v ∈ V ∖ N N ∈ G NeighbVtx v