Metamath Proof Explorer

Theorem rusgr1vtx

Description: If a k-regular simple graph has only one vertex, then k must be 0 . (Contributed by Alexander van der Vekens, 4-Sep-2018) (Revised by AV, 27-Dec-2020)

Ref Expression
Assertion rusgr1vtx ⊢Vtx⁡G=1∧GRegUSGraphK→K=0

Proof

Step Hyp Ref Expression
1 nbgr1vtx ⊢Vtx⁡G=1→GNeighbVtxv=∅
2 1 ralrimivw ⊢Vtx⁡G=1→∀v∈Vtx⁡GGNeighbVtxv=∅
3 eqid ⊢Vtx⁡G=Vtx⁡G
4 3 rusgrpropnb ⊢GRegUSGraphK→G∈USGraph∧K∈ℕ0*∧∀v∈Vtx⁡GGNeighbVtxv=K
5 2 4 anim12i ⊢Vtx⁡G=1∧GRegUSGraphK→∀v∈Vtx⁡GGNeighbVtxv=∅∧G∈USGraph∧K∈ℕ0*∧∀v∈Vtx⁡GGNeighbVtxv=K
6 fvex ⊢Vtx⁡G∈V
7 rusgr1vtxlem ⊢∀v∈Vtx⁡GGNeighbVtxv=K∧∀v∈Vtx⁡GGNeighbVtxv=∅∧Vtx⁡G∈V∧Vtx⁡G=1→K=0
8 7 ex ⊢∀v∈Vtx⁡GGNeighbVtxv=K∧∀v∈Vtx⁡GGNeighbVtxv=∅→Vtx⁡G∈V∧Vtx⁡G=1→K=0
9 6 8 mpani ⊢∀v∈Vtx⁡GGNeighbVtxv=K∧∀v∈Vtx⁡GGNeighbVtxv=∅→Vtx⁡G=1→K=0
10 9 ex ⊢∀v∈Vtx⁡GGNeighbVtxv=K→∀v∈Vtx⁡GGNeighbVtxv=∅→Vtx⁡G=1→K=0
11 10 3ad2ant3 ⊢G∈USGraph∧K∈ℕ0*∧∀v∈Vtx⁡GGNeighbVtxv=K→∀v∈Vtx⁡GGNeighbVtxv=∅→Vtx⁡G=1→K=0
12 11 com13 ⊢Vtx⁡G=1→∀v∈Vtx⁡GGNeighbVtxv=∅→G∈USGraph∧K∈ℕ0*∧∀v∈Vtx⁡GGNeighbVtxv=K→K=0
13 12 impd ⊢Vtx⁡G=1→∀v∈Vtx⁡GGNeighbVtxv=∅∧G∈USGraph∧K∈ℕ0*∧∀v∈Vtx⁡GGNeighbVtxv=K→K=0
14 13 adantr ⊢Vtx⁡G=1∧GRegUSGraphK→∀v∈Vtx⁡GGNeighbVtxv=∅∧G∈USGraph∧K∈ℕ0*∧∀v∈Vtx⁡GGNeighbVtxv=K→K=0
15 5 14 mpd ⊢Vtx⁡G=1∧GRegUSGraphK→K=0