Metamath Proof Explorer

Theorem lfgriswlk

Description: Conditions for a pair of functions to be a walk in a loop-free graph. (Contributed by AV, 28-Jan-2021)

Ref Expression
Hypotheses lfgrwlkprop.i ⊢I=iEdg⁡G
lfgriswlk.v ⊢V=Vtx⁡G
Assertion lfgriswlk ⊢G∈W∧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

Proof

Step Hyp Ref Expression
1 lfgrwlkprop.i ⊢I=iEdg⁡G
2 lfgriswlk.v ⊢V=Vtx⁡G
3 1 wlkf ⊢FWalks⁡GP→F∈Worddom⁡I
4 3 adantl ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧FWalks⁡GP→F∈Worddom⁡I
5 2 wlkp ⊢FWalks⁡GP→P:0…F⟶V
6 5 adantl ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧FWalks⁡GP→P:0…F⟶V
7 1 lfgrwlkprop ⊢FWalks⁡GP∧I:dom⁡I⟶x∈𝒫V|2≤x→∀k∈0..^FP⁡k≠P⁡k+1
8 7 expcom ⊢I:dom⁡I⟶x∈𝒫V|2≤x→FWalks⁡GP→∀k∈0..^FP⁡k≠P⁡k+1
9 8 adantl ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x→FWalks⁡GP→∀k∈0..^FP⁡k≠P⁡k+1
10 9 imp ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧FWalks⁡GP→∀k∈0..^FP⁡k≠P⁡k+1
11 1 wlkvtxeledg ⊢FWalks⁡GP→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k
12 11 adantl ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧FWalks⁡GP→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k
13 r19.26 ⊢∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k↔∀k∈0..^FP⁡k≠P⁡k+1∧∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k
14 10 12 13 sylanbrc ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧FWalks⁡GP→∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k
15 4 6 14 3jca ⊢G∈W∧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
16 simpr1 ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→F∈Worddom⁡I
17 simpr2 ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→P:0…F⟶V
18 df-ne ⊢P⁡k≠P⁡k+1↔¬P⁡k=P⁡k+1
19 ifpfal ⊢¬P⁡k=P⁡k+1→if-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k↔P⁡kP⁡k+1⊆I⁡F⁡k
20 18 19 sylbi ⊢P⁡k≠P⁡k+1→if-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k↔P⁡kP⁡k+1⊆I⁡F⁡k
21 20 biimpar ⊢P⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→if-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k
22 21 ralimi ⊢∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k
23 22 3ad2ant3 ⊢F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k
24 23 adantl ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k
25 2 1 iswlkg ⊢G∈W→FWalks⁡GP↔F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k
26 25 ad2antrr ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→FWalks⁡GP↔F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k
27 16 17 24 26 mpbir3and ⊢G∈W∧I:dom⁡I⟶x∈𝒫V|2≤x∧F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^FP⁡k≠P⁡k+1∧P⁡kP⁡k+1⊆I⁡F⁡k→FWalks⁡GP
28 15 27 impbida ⊢G∈W∧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