Metamath Proof Explorer

Theorem lfgrwlknloop

Description: In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021)

Ref Expression
Hypotheses lfgrwlkprop.i ⊢ I = iEdg ⁡ G
lfgriswlk.v ⊢ V = Vtx ⁡ G
Assertion lfgrwlknloop ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 lfgrwlkprop.i ⊢ I = iEdg ⁡ G
2 lfgriswlk.v ⊢ V = Vtx ⁡ G
3 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
4 1 2 lfgriswlk ⊢ G ∈ V ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
5 simpl ⊢ P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k ≠ P ⁡ k + 1
6 5 ralimi ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
7 6 3ad2ant3 ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
8 4 7 syl6bi ⊢ G ∈ V ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
9 8 ex ⊢ G ∈ V → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
10 9 com23 ⊢ G ∈ V → F Walks ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
11 10 3ad2ant1 ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
12 3 11 mpcom ⊢ F Walks ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
13 12 impcom ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1