clwlkclwwlk - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > clwlkclwwlk		Structured version Visualization version GIF version

Theorem clwlkclwwlk 27046

Description: A closed walk as word of length at least 2 corresponds to a closed walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 24-Apr-2021.)

**Hypotheses**
Ref	Expression
clwlkclwwlk.v	⊢ 𝑉 = (Vtx‘𝐺)
clwlkclwwlk.e	⊢ 𝐸 = (iEdg‘𝐺)

**Assertion**
Ref	Expression
clwlkclwwlk	⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺))))

Distinct variable groups: 𝑓,𝐸 𝑃,𝑓 𝑓,𝑉 𝑓,𝐺

Proof of Theorem clwlkclwwlk Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		clwlkclwwlk.e	. . . . . 6 ⊢ 𝐸 = (iEdg‘𝐺)
2	1	uspgrf1oedg 26188	. . . . 5 ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))
3		f1of1 6249	. . . . 5 ⊢ (𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺) → 𝐸:dom 𝐸–1-1→(Edg‘𝐺))
4	2, 3	syl 17	. . . 4 ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1→(Edg‘𝐺))
5		clwlkclwwlklem3 27045	. . . 4 ⊢ ((𝐸:dom 𝐸–1-1→(Edg‘𝐺) ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))))
6	4, 5	syl3an1 1472	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))))
7		lencl 13431	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℕ₀)
8		ige2m1fz 12544	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃)))
9	7, 8	sylan 489	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃)))
10		swrd0len 13542	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃))) → (♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = ((♯‘𝑃) − 1))
11	9, 10	syldan 488	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = ((♯‘𝑃) − 1))
12	7	nn0cnd 11466	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℂ)
13		1cnd 10169	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ)
14	12, 13	subcld 10505	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈ ℂ)
15	14	subid1d 10494	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ Word 𝑉 → (((♯‘𝑃) − 1) − 0) = ((♯‘𝑃) − 1))
16	15	eqcomd 2730	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) − 0))
17	16	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) − 0))
18	11, 17	eqtrd 2758	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = (((♯‘𝑃) − 1) − 0))
19	18	oveq1d 6780	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1) = ((((♯‘𝑃) − 1) − 0) − 1))
20	19	oveq2d 6781	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) = (0..^((((♯‘𝑃) − 1) − 0) − 1)))
21	11	oveq1d 6780	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1) = (((♯‘𝑃) − 1) − 1))
22	21	oveq2d 6781	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) = (0..^(((♯‘𝑃) − 1) − 1)))
23	22	eleq2d 2789	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) ↔ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))))
24		simpll 807	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑃 ∈ Word 𝑉)
25		wrdlenge2n0 13449	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ≠ ∅)
26	25	adantr 472	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑃 ≠ ∅)
27		nn0z 11513	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℤ)
28		peano2zm 11533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑃) ∈ ℤ → ((♯‘𝑃) − 1) ∈ ℤ)
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ∈ ℤ)
30	7, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈ ℤ)
31	30	adantr 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℤ)
32		elfzom1elfzo 12651	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝑃) − 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((♯‘𝑃) − 1)))
33	31, 32	sylan 489	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((♯‘𝑃) − 1)))
34		swrdtrcfv 13562	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖) = (𝑃‘𝑖))
35	24, 26, 33, 34	syl3anc 1439	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖) = (𝑃‘𝑖))
36	7	adantr 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘𝑃) ∈ ℕ₀)
37		elfzom1elp1fzo 12650	. . . . . . . . . . . . . . . . 17 ⊢ ((((♯‘𝑃) − 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
38	29, 37	sylan 489	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
39	36, 38	sylan 489	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
40		swrdtrcfv 13562	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
41	24, 26, 39, 40	syl3anc 1439	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
42	35, 41	preq12d 4383	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → {((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})
43	42	eleq1d 2788	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
44	43	ex 449	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1)) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))
45	23, 44	sylbid 230	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))
46	45	imp 444	. . . . . . . . 9 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1))) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
47	20, 46	raleqbidva 3257	. . . . . . . 8 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
48		swrdtrcfvl 13571	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = (𝑃‘((♯‘𝑃) − 2)))
49		swrdtrcfv0 13563	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0) = (𝑃‘0))
50	48, 49	preq12d 4383	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} = {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)})
51	50	eleq1d 2788	. . . . . . . 8 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ({( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))
52	47, 51	anbi12d 749	. . . . . . 7 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))
53	52	bicomd 213	. . . . . 6 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
54	53	3adant1 1122	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
55		swrdcl 13539	. . . . . . 7 ⊢ (𝑃 ∈ Word 𝑉 → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉)
56	55	3ad2ant2 1126	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉)
57	56	3biant1d 1554	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
58	54, 57	bitrd 268	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
59	58	anbi2d 742	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))))
60	6, 59	bitrd 268	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))))
61		uspgrupgr 26191	. . . . . 6 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)
62		clwlkclwwlk.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
63	62, 1	isclwlkupgr 26805	. . . . . . 7 ⊢ (𝐺 ∈ UPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))))))
64		3an4anass 1416	. . . . . . 7 ⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
65	63, 64	syl6bbr 278	. . . . . 6 ⊢ (𝐺 ∈ UPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
66	61, 65	syl 17	. . . . 5 ⊢ (𝐺 ∈ USPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
67	66	adantr 472	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
68	67	exbidv 1963	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
69	68	3adant3 1124	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
70		eqid 2724	. . . . . 6 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
71	62, 70	isclwwlk 27028	. . . . 5 ⊢ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺) ↔ (((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺)))
72		simpl 474	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ∈ Word 𝑉)
73		nn0ge2m1nn 11473	. . . . . . . . . . . 12 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℕ)
74	7, 73	sylan 489	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℕ)
75		nn0re 11414	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℝ)
76	75	lem1d 11070	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ≤ (♯‘𝑃))
77	76	a1d 25	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
78	7, 77	syl 17	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
79	78	imp 444	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃))
80	72, 74, 79	3jca 1379	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
81	80	3adant1 1122	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
82		swrdn0 13551	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)) → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅)
83	81, 82	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅)
84	83	biantrud 529	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅)))
85	84	bicomd 213	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅) ↔ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉))
86	85	3anbi1d 1516	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺))))
87	71, 86	syl5bb 272	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺))))
88		biid 251	. . . . 5 ⊢ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ↔ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉)
89		edgval 26061	. . . . . . . 8 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
90	1	eqcomi 2733	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = 𝐸
91	90	rneqi 5459	. . . . . . . 8 ⊢ ran (iEdg‘𝐺) = ran 𝐸
92	89, 91	eqtri 2746	. . . . . . 7 ⊢ (Edg‘𝐺) = ran 𝐸
93	92	eleq2i 2795	. . . . . 6 ⊢ ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
94	93	ralbii 3082	. . . . 5 ⊢ (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
95	92	eleq2i 2795	. . . . 5 ⊢ ({( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺) ↔ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)
96	88, 94, 95	3anbi123i 1388	. . . 4 ⊢ (((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))
97	87, 96	syl6bb 276	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
98	97	anbi2d 742	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))))
99	60, 69, 98	3bitr4d 300	1 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1072 = wceq 1596 ∃wex 1817 ∈ wcel 2103 ≠ wne 2896 ∀wral 3014 ∅c0 4023 {cpr 4287 ⟨cop 4291 class class class wbr 4760 dom cdm 5218 ran crn 5219 ⟶wf 5997 –1-1→wf1 5998 –1-1-onto→wf1o 6000 ‘cfv 6001 (class class class)co 6765 0cc0 10049 1c1 10050 + caddc 10052 ≤ cle 10188 − cmin 10379 ℕcn 11133 2c2 11183 ℕ₀cn0 11405 ℤcz 11490 ...cfz 12440 ..^cfzo 12580 ♯chash 13232 Word cword 13398 lastS clsw 13399 substr csubstr 13402 Vtxcvtx 25994 iEdgciedg 25995 Edgcedg 26059 UPGraphcupgr 26095 USPGraphcuspgr 26163 ClWalkscclwlks 26797 ClWWalkscclwwlk 27025

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-cnex 10105 ax-resscn 10106 ax-1cn 10107 ax-icn 10108 ax-addcl 10109 ax-addrcl 10110 ax-mulcl 10111 ax-mulrcl 10112 ax-mulcom 10113 ax-addass 10114 ax-mulass 10115 ax-distr 10116 ax-i2m1 10117 ax-1ne0 10118 ax-1rid 10119 ax-rnegex 10120 ax-rrecex 10121 ax-cnre 10122 ax-pre-lttri 10123 ax-pre-lttrn 10124 ax-pre-ltadd 10125 ax-pre-mulgt0 10126

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ifp 1051 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rmo 3022 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-uni 4545 df-int 4584 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-riota 6726 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-om 7183 df-1st 7285 df-2nd 7286 df-wrecs 7527 df-recs 7588 df-rdg 7626 df-1o 7680 df-2o 7681 df-oadd 7684 df-er 7862 df-map 7976 df-pm 7977 df-en 8073 df-dom 8074 df-sdom 8075 df-fin 8076 df-card 8878 df-cda 9103 df-pnf 10189 df-mnf 10190 df-xr 10191 df-ltxr 10192 df-le 10193 df-sub 10381 df-neg 10382 df-nn 11134 df-2 11192 df-n0 11406 df-xnn0 11477 df-z 11491 df-uz 11801 df-fz 12441 df-fzo 12581 df-hash 13233 df-word 13406 df-lsw 13407 df-substr 13410 df-edg 26060 df-uhgr 26073 df-upgr 26097 df-uspgr 26165 df-wlks 26626 df-clwlks 26798 df-clwwlk 27026

This theorem is referenced by: clwlkclwwlk2 27047 clwlkclwwlkf 27052

W3C validator