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∧FWalks⁡GP→∀k∈0..^FP⁡k≠P⁡k+1

Proof

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