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 ‘ 𝐺 ) ) = 1 ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐾 = 0 )

Proof

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