Metamath Proof Explorer

Theorem uvtxnbvtxm1

Description: A universal vertex has n - 1 neighbors in a finite simple graph with n vertices. A biconditional version of nbusgrvtxm1uvtx resp. uvtxnm1nbgr . (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020)

Ref Expression
Hypothesis uvtxnm1nbgr.v ⊢ V = Vtx ⁡ G
Assertion uvtxnbvtxm1 ⊢ G ∈ FinUSGraph ∧ U ∈ V → U ∈ UnivVtx ⁡ G ↔ G NeighbVtx U = V − 1

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v ⊢ V = Vtx ⁡ G
2 1 uvtxnm1nbgr ⊢ G ∈ FinUSGraph ∧ U ∈ UnivVtx ⁡ G → G NeighbVtx U = V − 1
3 2 ex ⊢ G ∈ FinUSGraph → U ∈ UnivVtx ⁡ G → G NeighbVtx U = V − 1
4 3 adantr ⊢ G ∈ FinUSGraph ∧ U ∈ V → U ∈ UnivVtx ⁡ G → G NeighbVtx U = V − 1
5 1 nbusgrvtxm1uvtx ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → U ∈ UnivVtx ⁡ G
6 4 5 impbid ⊢ G ∈ FinUSGraph ∧ U ∈ V → U ∈ UnivVtx ⁡ G ↔ G NeighbVtx U = V − 1