Theorem wlkf 28079

Description: The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)

Hypothesis

Ref	Expression
wlkf.i	⊢ 𝐼 = (iEdg‘𝐺)

Assertion

Ref	Expression
wlkf	⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)

Proof of Theorem wlkf

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2735	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		wlkf.i	. . 3 ⊢ 𝐼 = (iEdg‘𝐺)
3	1, 2	wlkprop 28076	. 2 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
4	3	simp1d 1141	1 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)

Syntax hints:   → wi 4  if-wif 1060   = wceq 1538   ∈ wcel 2103  ∀wral 3060   ⊆ wss 3891  {csn 4564  {cpr 4566   class class class wbr 5080  dom cdm 5600  ⟶wf 6454  ‘cfv 6458  (class class class)co 7308  0cc0 10931  1c1 10932   + caddc 10934  ...cfz 13299  ..^cfzo 13442  ♯chash 14104  Word cword 14276  Vtxcvtx 27464  iEdgciedg 27465  Walkscwlks 28061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-11 2151  ax-12 2168  ax-ext 2706  ax-rep 5217  ax-sep 5231  ax-nul 5238  ax-pow 5296  ax-pr 5360  ax-un 7621  ax-cnex 10987  ax-resscn 10988  ax-1cn 10989  ax-icn 10990  ax-addcl 10991  ax-addrcl 10992  ax-mulcl 10993  ax-mulrcl 10994  ax-mulcom 10995  ax-addass 10996  ax-mulass 10997  ax-distr 10998  ax-i2m1 10999  ax-1ne0 11000  ax-1rid 11001  ax-rnegex 11002  ax-rrecex 11003  ax-cnre 11004  ax-pre-lttri 11005  ax-pre-lttrn 11006  ax-pre-ltadd 11007  ax-pre-mulgt0 11008

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ifp 1061  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-nfc 2885  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3340  df-rab 3357  df-v 3438  df-sbc 3721  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4844  df-int 4886  df-iun 4932  df-br 5081  df-opab 5143  df-mpt 5164  df-tr 5198  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7265  df-ov 7311  df-oprab 7312  df-mpo 7313  df-om 7749  df-1st 7867  df-2nd 7868  df-frecs 8132  df-wrecs 8163  df-recs 8237  df-rdg 8276  df-1o 8332  df-er 8534  df-map 8653  df-en 8770  df-dom 8771  df-sdom 8772  df-fin 8773  df-card 9755  df-pnf 11071  df-mnf 11072  df-xr 11073  df-ltxr 11074  df-le 11075  df-sub 11267  df-neg 11268  df-nn 12034  df-n0 12294  df-z 12380  df-uz 12643  df-fz 13300  df-fzo 13443  df-hash 14105  df-word 14277  df-wlks 28064

This theorem is referenced by:  wlkcl  28080  wksvOLD  28085  iedginwlk  28102  wlk1ewlk  28105  wlkv0  28116  wlkonwlk1l  28129  wlkres  28136  redwlk  28138  wlkp1lem2  28140  wlkp1lem3  28141  wlkp1lem4  28142  wlkp1lem6  28144  wlkp1lem8  28146  wlkp1  28147  lfgriswlk  28154  trlf1  28164  trlreslem  28165  upgr2pthnlp  28198  uhgrwkspthlem1  28219  usgr2wlkspthlem1  28223  crctcshlem2  28281  crctcshlem4  28283  crctcshwlkn0  28284  eupth2eucrct  28679  eucrctshift  28705  eucrct2eupth  28707  pfxwlk  33181  revwlk  33182  swrdwlk  33184