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 27787

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.) (Revised by AV, 30-Oct-2022.)

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

**Assertion**
Ref	Expression
clwlkclwwlk	⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (𝑃 prefix ((♯‘𝑃) − 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 26966	. . . . 5 ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))
3		f1of1 6589	. . . . 5 ⊢ (𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺) → 𝐸:dom 𝐸–1-1→(Edg‘𝐺))
4	2, 3	syl 17	. . . 4 ⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1→(Edg‘𝐺))
5		clwlkclwwlklem3 27786	. . . 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 1160	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))))
7		lencl 13876	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℕ₀)
8		ige2m1fz 12992	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃)))
9	7, 8	sylan 583	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃)))
10		pfxlen 14036	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃))) → (♯‘(𝑃 prefix ((♯‘𝑃) − 1))) = ((♯‘𝑃) − 1))
11	9, 10	syldan 594	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 prefix ((♯‘𝑃) − 1))) = ((♯‘𝑃) − 1))
12	7	nn0cnd 11945	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℂ)
13		1cnd 10625	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ)
14	12, 13	subcld 10986	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈ ℂ)
15	14	subid1d 10975	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ Word 𝑉 → (((♯‘𝑃) − 1) − 0) = ((♯‘𝑃) − 1))
16	15	eqcomd 2804	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) − 0))
17	16	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) − 0))
18	11, 17	eqtrd 2833	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 prefix ((♯‘𝑃) − 1))) = (((♯‘𝑃) − 1) − 0))
19	18	oveq1d 7150	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1) = ((((♯‘𝑃) − 1) − 0) − 1))
20	19	oveq2d 7151	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)) = (0..^((((♯‘𝑃) − 1) − 0) − 1)))
21	11	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1) = (((♯‘𝑃) − 1) − 1))
22	21	oveq2d 7151	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)) = (0..^(((♯‘𝑃) − 1) − 1)))
23	22	eleq2d 2875	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)) ↔ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))))
24		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑃 ∈ Word 𝑉)
25		wrdlenge2n0 13895	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ≠ ∅)
26	25	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑃 ≠ ∅)
27		nn0z 11993	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℤ)
28		peano2zm 12013	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑃) ∈ ℤ → ((♯‘𝑃) − 1) ∈ ℤ)
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ∈ ℤ)
30	7, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈ ℤ)
31	30	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℤ)
32		elfzom1elfzo 13100	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘𝑃) − 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((♯‘𝑃) − 1)))
33	31, 32	sylan 583	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((♯‘𝑃) − 1)))
34		pfxtrcfv 14046	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖) = (𝑃‘𝑖))
35	24, 26, 33, 34	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖) = (𝑃‘𝑖))
36	7	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘𝑃) ∈ ℕ₀)
37		elfzom1elp1fzo 13099	. . . . . . . . . . . . . . . . 17 ⊢ ((((♯‘𝑃) − 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
38	29, 37	sylan 583	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
39	36, 38	sylan 583	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
40		pfxtrcfv 14046	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
41	24, 26, 39, 40	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
42	35, 41	preq12d 4637	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → {((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})
43	42	eleq1d 2874	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ({((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
44	43	ex 416	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1)) → ({((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))
45	23, 44	sylbid 243	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)) → ({((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))
46	45	imp 410	. . . . . . . . 9 ⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1))) → ({((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
47	20, 46	raleqbidva 3370	. . . . . . . 8 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
48		pfxtrcfvl 14050	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (lastS‘(𝑃 prefix ((♯‘𝑃) − 1))) = (𝑃‘((♯‘𝑃) − 2)))
49		pfxtrcfv0 14047	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 prefix ((♯‘𝑃) − 1))‘0) = (𝑃‘0))
50	48, 49	preq12d 4637	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} = {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)})
51	50	eleq1d 2874	. . . . . . . 8 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ({(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))
52	47, 51	anbi12d 633	. . . . . . 7 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))
53	52	bicomd 226	. . . . . 6 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸)))
54	53	3adant1 1127	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸)))
55		pfxcl 14030	. . . . . . 7 ⊢ (𝑃 ∈ Word 𝑉 → (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉)
56	55	3ad2ant2 1131	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉)
57	56	3biant1d 1475	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸) ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸)))
58	54, 57	bitrd 282	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸)))
59	58	anbi2d 631	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸))))
60	6, 59	bitrd 282	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸))))
61		uspgrupgr 26969	. . . . . 6 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)
62		clwlkclwwlk.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
63	62, 1	isclwlkupgr 27567	. . . . . . 7 ⊢ (𝐺 ∈ UPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))))))
64		3an4anass 1102	. . . . . . 7 ⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
65	63, 64	syl6bbr 292	. . . . . 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 484	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
68	67	exbidv 1922	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
69	68	3adant3 1129	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
70		eqid 2798	. . . . . 6 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
71	62, 70	isclwwlk 27769	. . . . 5 ⊢ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ (ClWWalks‘𝐺) ↔ (((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ (Edg‘𝐺)))
72		simpl 486	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ∈ Word 𝑉)
73		nn0ge2m1nn 11952	. . . . . . . . . . . 12 ⊢ (((♯‘𝑃) ∈ ℕ₀ ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℕ)
74	7, 73	sylan 583	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℕ)
75		nn0re 11894	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (♯‘𝑃) ∈ ℝ)
76	75	lem1d 11562	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑃) ∈ ℕ₀ → ((♯‘𝑃) − 1) ≤ (♯‘𝑃))
77	76	a1d 25	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑃) ∈ ℕ₀ → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
78	7, 77	syl 17	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
79	78	imp 410	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃))
80	72, 74, 79	3jca 1125	. . . . . . . . . 10 ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
81	80	3adant1 1127	. . . . . . . . 9 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
82		pfxn0 14039	. . . . . . . . 9 ⊢ ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)) → (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅)
83	81, 82	syl 17	. . . . . . . 8 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅)
84	83	biantrud 535	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅)))
85	84	bicomd 226	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅) ↔ (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉))
86	85	3anbi1d 1437	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ (Edg‘𝐺))))
87	71, 86	syl5bb 286	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ (ClWWalks‘𝐺) ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ (Edg‘𝐺))))
88		biid 264	. . . . 5 ⊢ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ↔ (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉)
89		edgval 26842	. . . . . . . 8 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
90	1	eqcomi 2807	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = 𝐸
91	90	rneqi 5771	. . . . . . . 8 ⊢ ran (iEdg‘𝐺) = ran 𝐸
92	89, 91	eqtri 2821	. . . . . . 7 ⊢ (Edg‘𝐺) = ran 𝐸
93	92	eleq2i 2881	. . . . . 6 ⊢ ({((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸)
94	93	ralbii 3133	. . . . 5 ⊢ (∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸)
95	92	eleq2i 2881	. . . . 5 ⊢ ({(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ (Edg‘𝐺) ↔ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸)
96	88, 94, 95	3anbi123i 1152	. . . 4 ⊢ (((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸))
97	87, 96	syl6bb 290	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ (ClWWalks‘𝐺) ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸)))
98	97	anbi2d 631	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ∈ (ClWWalks‘𝐺)) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸))))
99	60, 69, 98	3bitr4d 314	1 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ∈ (ClWWalks‘𝐺))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∅c0 4243 {cpr 4527 class class class wbr 5030 dom cdm 5519 ran crn 5520 ⟶wf 6320 –1-1→wf1 6321 –1-1-onto→wf1o 6323 ‘cfv 6324 (class class class)co 7135 0cc0 10526 1c1 10527 + caddc 10529 ≤ cle 10665 − cmin 10859 ℕcn 11625 2c2 11680 ℕ₀cn0 11885 ℤcz 11969 ...cfz 12885 ..^cfzo 13028 ♯chash 13686 Word cword 13857 lastSclsw 13905 prefix cpfx 14023 Vtxcvtx 26789 iEdgciedg 26790 Edgcedg 26840 UPGraphcupgr 26873 USPGraphcuspgr 26941 ClWalkscclwlks 27559 ClWWalkscclwwlk 27766

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ifp 1059 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-map 8391 df-pm 8392 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-dju 9314 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-nn 11626 df-2 11688 df-n0 11886 df-xnn0 11956 df-z 11970 df-uz 12232 df-fz 12886 df-fzo 13029 df-hash 13687 df-word 13858 df-lsw 13906 df-substr 13994 df-pfx 14024 df-edg 26841 df-uhgr 26851 df-upgr 26875 df-uspgr 26943 df-wlks 27389 df-clwlks 27560 df-clwwlk 27767

This theorem is referenced by: clwlkclwwlk2 27788 clwlkclwwlkf 27793

W3C validator