Metamath Proof Explorer

Theorem wwlknbp1

Description: Other basic properties of a walk of a fixed length as word. (Contributed by AV, 8-Mar-2022)

Ref Expression
Assertion wwlknbp1 ⊢W∈NWWalksNG→N∈ℕ0∧W∈WordVtx⁡G∧W=N+1

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 1 wwlknbp ⊢W∈NWWalksNG→G∈V∧N∈ℕ0∧W∈WordVtx⁡G
3 eqid ⊢Edg⁡G=Edg⁡G
4 1 3 wwlknp ⊢W∈NWWalksNG→W∈WordVtx⁡G∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G
5 simpl ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G→N∈ℕ0
6 simpr1 ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G→W∈WordVtx⁡G
7 simpr2 ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G→W=N+1
8 5 6 7 3jca ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G→N∈ℕ0∧W∈WordVtx⁡G∧W=N+1
9 8 ex ⊢N∈ℕ0→W∈WordVtx⁡G∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G→N∈ℕ0∧W∈WordVtx⁡G∧W=N+1
10 9 3ad2ant2 ⊢G∈V∧N∈ℕ0∧W∈WordVtx⁡G→W∈WordVtx⁡G∧W=N+1∧∀i∈0..^NW⁡iW⁡i+1∈Edg⁡G→N∈ℕ0∧W∈WordVtx⁡G∧W=N+1
11 2 4 10 sylc ⊢W∈NWWalksNG→N∈ℕ0∧W∈WordVtx⁡G∧W=N+1