| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | clwlkclwwlk.e | . . . . . 6
⊢ 𝐸 = (iEdg‘𝐺) | 
| 2 | 1 | uspgrf1oedg 29191 | . . . . 5
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) | 
| 3 |  | f1of1 6846 | . . . . 5
⊢ (𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺) → 𝐸:dom 𝐸–1-1→(Edg‘𝐺)) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1→(Edg‘𝐺)) | 
| 5 |  | clwlkclwwlklem3 30021 | . . . 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 1163 | . . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) | 
| 7 |  | lencl 14572 | . . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈
ℕ0) | 
| 8 |  | ige2m1fz 13658 | . . . . . . . . . . . . . 14
⊢
(((♯‘𝑃)
∈ ℕ0 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈
(0...(♯‘𝑃))) | 
| 9 | 7, 8 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈
(0...(♯‘𝑃))) | 
| 10 |  | pfxlen 14722 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈
(0...(♯‘𝑃)))
→ (♯‘(𝑃
prefix ((♯‘𝑃)
− 1))) = ((♯‘𝑃) − 1)) | 
| 11 | 9, 10 | syldan 591 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 prefix ((♯‘𝑃) − 1))) =
((♯‘𝑃) −
1)) | 
| 12 | 7 | nn0cnd 12591 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℂ) | 
| 13 |  | 1cnd 11257 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ) | 
| 14 | 12, 13 | subcld 11621 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈
ℂ) | 
| 15 | 14 | subid1d 11610 | . . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (((♯‘𝑃) − 1) − 0) =
((♯‘𝑃) −
1)) | 
| 16 | 15 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) −
0)) | 
| 17 | 16 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) =
(((♯‘𝑃) −
1) − 0)) | 
| 18 | 11, 17 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 prefix ((♯‘𝑃) − 1))) =
(((♯‘𝑃) −
1) − 0)) | 
| 19 | 18 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1) =
((((♯‘𝑃)
− 1) − 0) − 1)) | 
| 20 | 19 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) →
(0..^((♯‘(𝑃
prefix ((♯‘𝑃)
− 1))) − 1)) = (0..^((((♯‘𝑃) − 1) − 0) −
1))) | 
| 21 | 11 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1) =
(((♯‘𝑃) −
1) − 1)) | 
| 22 | 21 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) →
(0..^((♯‘(𝑃
prefix ((♯‘𝑃)
− 1))) − 1)) = (0..^(((♯‘𝑃) − 1) − 1))) | 
| 23 | 22 | eleq2d 2826 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1))
↔ 𝑖 ∈
(0..^(((♯‘𝑃)
− 1) − 1)))) | 
| 24 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
𝑃 ∈ Word 𝑉) | 
| 25 |  | wrdlenge2n0 14591 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ≠ ∅) | 
| 26 | 25 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
𝑃 ≠
∅) | 
| 27 |  | nn0z 12640 | . . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑃)
∈ ℕ0 → (♯‘𝑃) ∈ ℤ) | 
| 28 |  | peano2zm 12662 | . . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑃)
∈ ℤ → ((♯‘𝑃) − 1) ∈
ℤ) | 
| 29 | 27, 28 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑃)
∈ ℕ0 → ((♯‘𝑃) − 1) ∈
ℤ) | 
| 30 | 7, 29 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈
ℤ) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈
ℤ) | 
| 32 |  | elfzom1elfzo 13773 | . . . . . . . . . . . . . . . 16
⊢
((((♯‘𝑃)
− 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
𝑖 ∈
(0..^((♯‘𝑃)
− 1))) | 
| 33 | 31, 32 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
𝑖 ∈
(0..^((♯‘𝑃)
− 1))) | 
| 34 |  | pfxtrcfv 14732 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖) = (𝑃‘𝑖)) | 
| 35 | 24, 26, 33, 34 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
((𝑃 prefix
((♯‘𝑃) −
1))‘𝑖) = (𝑃‘𝑖)) | 
| 36 | 7 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘𝑃) ∈
ℕ0) | 
| 37 |  | elfzom1elp1fzo 13772 | . . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝑃)
− 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
(𝑖 + 1) ∈
(0..^((♯‘𝑃)
− 1))) | 
| 38 | 29, 37 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢
(((♯‘𝑃)
∈ ℕ0 ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
(𝑖 + 1) ∈
(0..^((♯‘𝑃)
− 1))) | 
| 39 | 36, 38 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
(𝑖 + 1) ∈
(0..^((♯‘𝑃)
− 1))) | 
| 40 |  | pfxtrcfv 14732 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) | 
| 41 | 24, 26, 39, 40 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
((𝑃 prefix
((♯‘𝑃) −
1))‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) | 
| 42 | 35, 41 | preq12d 4740 | . . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
{((𝑃 prefix
((♯‘𝑃) −
1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) | 
| 43 | 42 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) →
({((𝑃 prefix
((♯‘𝑃) −
1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) | 
| 44 | 43 | ex 412 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1)) →
({((𝑃 prefix
((♯‘𝑃) −
1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) | 
| 45 | 23, 44 | sylbid 240 | . . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1))
→ ({((𝑃 prefix
((♯‘𝑃) −
1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) | 
| 46 | 45 | imp 406 | . . . . . . . . 9
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) − 1)))
→ ({((𝑃 prefix
((♯‘𝑃) −
1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) | 
| 47 | 20, 46 | raleqbidva 3331 | . . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∀𝑖 ∈
(0..^((♯‘(𝑃
prefix ((♯‘𝑃)
− 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) | 
| 48 |  | pfxtrcfvl 14736 | . . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (lastS‘(𝑃 prefix ((♯‘𝑃) − 1))) = (𝑃‘((♯‘𝑃) − 2))) | 
| 49 |  | pfxtrcfv0 14733 | . . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 prefix ((♯‘𝑃) − 1))‘0) = (𝑃‘0)) | 
| 50 | 48, 49 | preq12d 4740 | . . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} =
{(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)}) | 
| 51 | 50 | eleq1d 2825 | . . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ({(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈
ran 𝐸 ↔ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) | 
| 52 | 47, 51 | anbi12d 632 | . . . . . . 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 223 | . . . . . 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 1130 | . . . . 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 14716 | . . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉) | 
| 56 | 55 | 3ad2ant2 1134 | . . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉) | 
| 57 | 56 | 3biant1d 1479 | . . . . 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 279 | . . . 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 630 | . . 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 279 | . 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 29196 | . . . . . 6
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈
UPGraph) | 
| 62 |  | clwlkclwwlk.v | . . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) | 
| 63 | 62, 1 | isclwlkupgr 29799 | . . . . . . 7
⊢ (𝐺 ∈ UPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))) | 
| 64 |  | 3an4anass 1104 | . . . . . . 7
⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))))) | 
| 65 | 63, 64 | bitr4di 289 | . . . . . 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 480 | . . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))))) | 
| 68 | 67 | exbidv 1920 | . . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))))) | 
| 69 | 68 | 3adant3 1132 | . 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))))) | 
| 70 |  | eqid 2736 | . . . . . 6
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 71 | 62, 70 | isclwwlk 30004 | . . . . 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 482 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ∈ Word 𝑉) | 
| 73 |  | nn0ge2m1nn 12598 | . . . . . . . . . . . 12
⊢
(((♯‘𝑃)
∈ ℕ0 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈
ℕ) | 
| 74 | 7, 73 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈
ℕ) | 
| 75 |  | nn0re 12537 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝑃)
∈ ℕ0 → (♯‘𝑃) ∈ ℝ) | 
| 76 | 75 | lem1d 12202 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑃)
∈ ℕ0 → ((♯‘𝑃) − 1) ≤ (♯‘𝑃)) | 
| 77 | 76 | a1d 25 | . . . . . . . . . . . . 13
⊢
((♯‘𝑃)
∈ ℕ0 → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃))) | 
| 78 | 7, 77 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤
(♯‘𝑃))) | 
| 79 | 78 | imp 406 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ≤
(♯‘𝑃)) | 
| 80 | 72, 74, 79 | 3jca 1128 | . . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧
((♯‘𝑃) −
1) ≤ (♯‘𝑃))) | 
| 81 | 80 | 3adant1 1130 | . . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧
((♯‘𝑃) −
1) ≤ (♯‘𝑃))) | 
| 82 |  | pfxn0 14725 | . . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧
((♯‘𝑃) −
1) ≤ (♯‘𝑃))
→ (𝑃 prefix
((♯‘𝑃) −
1)) ≠ ∅) | 
| 83 | 81, 82 | syl 17 | . . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅) | 
| 84 | 83 | biantrud 531 | . . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ↔ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ≠
∅))) | 
| 85 | 84 | bicomd 223 | . . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ≠ ∅) ↔ (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉)) | 
| 86 | 85 | 3anbi1d 1441 | . . . . 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 | bitrid 283 | . . . 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 261 | . . . . 5
⊢ ((𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉 ↔ (𝑃 prefix ((♯‘𝑃) − 1)) ∈ Word 𝑉) | 
| 89 |  | edgval 29067 | . . . . . . . 8
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) | 
| 90 | 1 | eqcomi 2745 | . . . . . . . . 9
⊢
(iEdg‘𝐺) =
𝐸 | 
| 91 | 90 | rneqi 5947 | . . . . . . . 8
⊢ ran
(iEdg‘𝐺) = ran 𝐸 | 
| 92 | 89, 91 | eqtri 2764 | . . . . . . 7
⊢
(Edg‘𝐺) = ran
𝐸 | 
| 93 | 92 | eleq2i 2832 | . . . . . 6
⊢ ({((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸) | 
| 94 | 93 | ralbii 3092 | . . . . 5
⊢
(∀𝑖 ∈
(0..^((♯‘(𝑃
prefix ((♯‘𝑃)
− 1))) − 1)){((𝑃 prefix ((♯‘𝑃) − 1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝑃 prefix ((♯‘𝑃) − 1))) −
1)){((𝑃 prefix
((♯‘𝑃) −
1))‘𝑖), ((𝑃 prefix ((♯‘𝑃) − 1))‘(𝑖 + 1))} ∈ ran 𝐸) | 
| 95 | 92 | eleq2i 2832 | . . . . 5
⊢
({(lastS‘(𝑃
prefix ((♯‘𝑃)
− 1))), ((𝑃 prefix
((♯‘𝑃) −
1))‘0)} ∈ (Edg‘𝐺) ↔ {(lastS‘(𝑃 prefix ((♯‘𝑃) − 1))), ((𝑃 prefix ((♯‘𝑃) − 1))‘0)} ∈ ran 𝐸) | 
| 96 | 88, 94, 95 | 3anbi123i 1155 | . . . 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 | bitrdi 287 | . . 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 630 | . 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 311 | 1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (𝑃 prefix ((♯‘𝑃) − 1)) ∈ (ClWWalks‘𝐺)))) |