Theorem iswlk 28022

Description: Properties of a pair of functions to be a walk. (Contributed by AV, 30-Dec-2020.)

Hypotheses

Ref	Expression
wksfval.v	⊢ 𝑉 = (Vtx‘𝐺)
wksfval.i	⊢ 𝐼 = (iEdg‘𝐺)

Assertion

Ref	Expression
iswlk	⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))

Distinct variable groups:   𝑘,𝐺   𝑘,𝐹   𝑃,𝑘

Allowed substitution hints:   𝑈(𝑘)   𝐼(𝑘)   𝑉(𝑘)   𝑊(𝑘)   𝑍(𝑘)

Proof of Theorem iswlk

Dummy variables 𝑓 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-br 5082	. . 3 ⊢ (𝐹(Walks‘𝐺)𝑃 ↔ ⟨𝐹, 𝑃⟩ ∈ (Walks‘𝐺))
2		wksfval.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
3		wksfval.i	. . . . . 6 ⊢ 𝐼 = (iEdg‘𝐺)
4	2, 3	wksfval 28021	. . . . 5 ⊢ (𝐺 ∈ 𝑊 → (Walks‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))})
5	4	3ad2ant1 1133	. . . 4 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (Walks‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))})
6	5	eleq2d 2822	. . 3 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (⟨𝐹, 𝑃⟩ ∈ (Walks‘𝐺) ↔ ⟨𝐹, 𝑃⟩ ∈ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))}))
7	1, 6	bitrid 283	. 2 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ ⟨𝐹, 𝑃⟩ ∈ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))}))
8		eleq1 2824	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼))
9	8	adantr 482	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼))
10		simpr 486	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃)
11		fveq2 6804	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (♯‘𝑓) = (♯‘𝐹))
12	11	oveq2d 7323	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (0...(♯‘𝑓)) = (0...(♯‘𝐹)))
13	12	adantr 482	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (0...(♯‘𝑓)) = (0...(♯‘𝐹)))
14	10, 13	feq12d 6618	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝:(0...(♯‘𝑓))⟶𝑉 ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉))
15	11	oveq2d 7323	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (0..^(♯‘𝑓)) = (0..^(♯‘𝐹)))
16	15	adantr 482	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (0..^(♯‘𝑓)) = (0..^(♯‘𝐹)))
17		fveq1 6803	. . . . . . . . 9 ⊢ (𝑝 = 𝑃 → (𝑝‘𝑘) = (𝑃‘𝑘))
18		fveq1 6803	. . . . . . . . 9 ⊢ (𝑝 = 𝑃 → (𝑝‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)))
19	17, 18	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑝 = 𝑃 → ((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) ↔ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1))))
20	19	adantl 483	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) ↔ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1))))
21		fveq1 6803	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑘) = (𝐹‘𝑘))
22	21	fveq2d 6808	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝐼‘(𝑓‘𝑘)) = (𝐼‘(𝐹‘𝑘)))
23	17	sneqd 4577	. . . . . . . 8 ⊢ (𝑝 = 𝑃 → {(𝑝‘𝑘)} = {(𝑃‘𝑘)})
24	22, 23	eqeqan12d 2750	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)} ↔ (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}))
25	17, 18	preq12d 4681	. . . . . . . . 9 ⊢ (𝑝 = 𝑃 → {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})
26	25	adantl 483	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})
27	22	adantr 482	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝐼‘(𝑓‘𝑘)) = (𝐼‘(𝐹‘𝑘)))
28	26, 27	sseq12d 3959	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ({(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)) ↔ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
29	20, 24, 28	ifpbi123d 1078	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
30	16, 29	raleqbidv 3348	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))) ↔ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
31	9, 14, 30	3anbi123d 1436	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘)))) ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
32	31	opelopabga 5459	. . 3 ⊢ ((𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (⟨𝐹, 𝑃⟩ ∈ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))} ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
33	32	3adant1 1130	. 2 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (⟨𝐹, 𝑃⟩ ∈ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))} ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
34	7, 33	bitrd 279	1 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  if-wif 1061   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104  ∀wral 3062   ⊆ wss 3892  {csn 4565  {cpr 4567  ⟨cop 4571   class class class wbr 5081  {copab 5143  dom cdm 5600  ⟶wf 6454  ‘cfv 6458  (class class class)co 7307  0cc0 10917  1c1 10918   + caddc 10920  ...cfz 13285  ..^cfzo 13428  ♯chash 14090  Word cword 14262  Vtxcvtx 27411  iEdgciedg 27412  Walkscwlks 28008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-cnex 10973  ax-resscn 10974  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-mulcom 10981  ax-addass 10982  ax-mulass 10983  ax-distr 10984  ax-i2m1 10985  ax-1ne0 10986  ax-1rid 10987  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990  ax-pre-lttri 10991  ax-pre-lttrn 10992  ax-pre-ltadd 10993  ax-pre-mulgt0 10994

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ifp 1062  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  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 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-om 7745  df-1st 7863  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-1o 8328  df-er 8529  df-map 8648  df-en 8765  df-dom 8766  df-sdom 8767  df-fin 8768  df-card 9741  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-le 11061  df-sub 11253  df-neg 11254  df-nn 12020  df-n0 12280  df-z 12366  df-uz 12629  df-fz 13286  df-fzo 13429  df-hash 14091  df-word 14263  df-wlks 28011

This theorem is referenced by:  wlkprop  28023  iswlkg  28025  wlkvtxeledg  28036  wlk1walk  28051  redwlk  28085  wlkp1  28094  wlkd  28099  lfgrwlkprop  28100  crctcshwlkn0  28231  upwlkwlk  45359  upgrwlkupwlk  45360