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 ∧ G RegUSGraph K → K = 0

Proof

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