Metamath Proof Explorer

Theorem uvtx2vtx1edg

Description: If a graph has two vertices, and there is an edge between the vertices, then each vertex is universal. (Contributed by AV, 1-Nov-2020) (Revised by AV, 25-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypotheses uvtxel.v ⊢ V = Vtx ⁡ G
isuvtx.e ⊢ E = Edg ⁡ G
Assertion uvtx2vtx1edg ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V v ∈ UnivVtx ⁡ G

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 isuvtx.e ⊢ E = Edg ⁡ G
3 1 2 nbgr2vtx1edg ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
4 1 uvtxel ⊢ v ∈ UnivVtx ⁡ G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
5 4 a1i ⊢ V = 2 ∧ V ∈ E → v ∈ UnivVtx ⁡ G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
6 5 baibd ⊢ V = 2 ∧ V ∈ E ∧ v ∈ V → v ∈ UnivVtx ⁡ G ↔ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
7 6 ralbidva ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V v ∈ UnivVtx ⁡ G ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
8 3 7 mpbird ⊢ V = 2 ∧ V ∈ E → ∀ v ∈ V v ∈ UnivVtx ⁡ G