Step | Hyp | Ref
| Expression |
1 | | clwlkclwwlkf.c |
. . . . 5
⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} |
2 | | eqid 2739 |
. . . . 5
⊢
(1st ‘𝑐) = (1st ‘𝑐) |
3 | | eqid 2739 |
. . . . 5
⊢
(2nd ‘𝑐) = (2nd ‘𝑐) |
4 | 1, 2, 3 | clwlkclwwlkflem 28347 |
. . . 4
⊢ (𝑐 ∈ 𝐶 → ((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ)) |
5 | | isclwlk 28120 |
. . . . . . . 8
⊢
((1st ‘𝑐)(ClWalks‘𝐺)(2nd ‘𝑐) ↔ ((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))))) |
6 | | fvex 6781 |
. . . . . . . . 9
⊢
(1st ‘𝑐) ∈ V |
7 | | breq1 5081 |
. . . . . . . . 9
⊢ (𝑓 = (1st ‘𝑐) → (𝑓(ClWalks‘𝐺)(2nd ‘𝑐) ↔ (1st ‘𝑐)(ClWalks‘𝐺)(2nd ‘𝑐))) |
8 | 6, 7 | spcev 3543 |
. . . . . . . 8
⊢
((1st ‘𝑐)(ClWalks‘𝐺)(2nd ‘𝑐) → ∃𝑓 𝑓(ClWalks‘𝐺)(2nd ‘𝑐)) |
9 | 5, 8 | sylbir 234 |
. . . . . . 7
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐)))) →
∃𝑓 𝑓(ClWalks‘𝐺)(2nd ‘𝑐)) |
10 | 9 | 3adant3 1130 |
. . . . . 6
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ) → ∃𝑓 𝑓(ClWalks‘𝐺)(2nd ‘𝑐)) |
11 | 10 | adantl 481 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ)) → ∃𝑓 𝑓(ClWalks‘𝐺)(2nd ‘𝑐)) |
12 | | simpl 482 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ)) → 𝐺 ∈ USPGraph) |
13 | | eqid 2739 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
14 | 13 | wlkpwrd 27965 |
. . . . . . . 8
⊢
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (2nd ‘𝑐) ∈ Word (Vtx‘𝐺)) |
15 | 14 | 3ad2ant1 1131 |
. . . . . . 7
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ) → (2nd
‘𝑐) ∈ Word
(Vtx‘𝐺)) |
16 | 15 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ)) → (2nd
‘𝑐) ∈ Word
(Vtx‘𝐺)) |
17 | | elnnnn0c 12261 |
. . . . . . . . . 10
⊢
((♯‘(1st ‘𝑐)) ∈ ℕ ↔
((♯‘(1st ‘𝑐)) ∈ ℕ0 ∧ 1 ≤
(♯‘(1st ‘𝑐)))) |
18 | | nn0re 12225 |
. . . . . . . . . . . . . 14
⊢
((♯‘(1st ‘𝑐)) ∈ ℕ0 →
(♯‘(1st ‘𝑐)) ∈ ℝ) |
19 | | 1e2m1 12083 |
. . . . . . . . . . . . . . . . 17
⊢ 1 = (2
− 1) |
20 | 19 | breq1i 5085 |
. . . . . . . . . . . . . . . 16
⊢ (1 ≤
(♯‘(1st ‘𝑐)) ↔ (2 − 1) ≤
(♯‘(1st ‘𝑐))) |
21 | 20 | biimpi 215 |
. . . . . . . . . . . . . . 15
⊢ (1 ≤
(♯‘(1st ‘𝑐)) → (2 − 1) ≤
(♯‘(1st ‘𝑐))) |
22 | | 2re 12030 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
23 | | 1re 10959 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
24 | | lesubadd 11430 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘(1st
‘𝑐)) ∈ ℝ)
→ ((2 − 1) ≤ (♯‘(1st ‘𝑐)) ↔ 2 ≤
((♯‘(1st ‘𝑐)) + 1))) |
25 | 22, 23, 24 | mp3an12 1449 |
. . . . . . . . . . . . . . 15
⊢
((♯‘(1st ‘𝑐)) ∈ ℝ → ((2 − 1) ≤
(♯‘(1st ‘𝑐)) ↔ 2 ≤
((♯‘(1st ‘𝑐)) + 1))) |
26 | 21, 25 | syl5ib 243 |
. . . . . . . . . . . . . 14
⊢
((♯‘(1st ‘𝑐)) ∈ ℝ → (1 ≤
(♯‘(1st ‘𝑐)) → 2 ≤
((♯‘(1st ‘𝑐)) + 1))) |
27 | 18, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢
((♯‘(1st ‘𝑐)) ∈ ℕ0 → (1 ≤
(♯‘(1st ‘𝑐)) → 2 ≤
((♯‘(1st ‘𝑐)) + 1))) |
28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ (♯‘(1st
‘𝑐)) ∈
ℕ0) → (1 ≤ (♯‘(1st ‘𝑐)) → 2 ≤
((♯‘(1st ‘𝑐)) + 1))) |
29 | | wlklenvp1 27966 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (♯‘(2nd
‘𝑐)) =
((♯‘(1st ‘𝑐)) + 1)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ (♯‘(1st
‘𝑐)) ∈
ℕ0) → (♯‘(2nd ‘𝑐)) =
((♯‘(1st ‘𝑐)) + 1)) |
31 | 30 | breq2d 5090 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ (♯‘(1st
‘𝑐)) ∈
ℕ0) → (2 ≤ (♯‘(2nd ‘𝑐)) ↔ 2 ≤
((♯‘(1st ‘𝑐)) + 1))) |
32 | 28, 31 | sylibrd 258 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ (♯‘(1st
‘𝑐)) ∈
ℕ0) → (1 ≤ (♯‘(1st ‘𝑐)) → 2 ≤
(♯‘(2nd ‘𝑐)))) |
33 | 32 | expimpd 453 |
. . . . . . . . . 10
⊢
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (((♯‘(1st
‘𝑐)) ∈
ℕ0 ∧ 1 ≤ (♯‘(1st ‘𝑐))) → 2 ≤
(♯‘(2nd ‘𝑐)))) |
34 | 17, 33 | syl5bi 241 |
. . . . . . . . 9
⊢
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → ((♯‘(1st
‘𝑐)) ∈ ℕ
→ 2 ≤ (♯‘(2nd ‘𝑐)))) |
35 | 34 | a1d 25 |
. . . . . . . 8
⊢
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) →
((♯‘(1st ‘𝑐)) ∈ ℕ → 2 ≤
(♯‘(2nd ‘𝑐))))) |
36 | 35 | 3imp 1109 |
. . . . . . 7
⊢
(((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ) → 2 ≤
(♯‘(2nd ‘𝑐))) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ)) → 2 ≤
(♯‘(2nd ‘𝑐))) |
38 | | eqid 2739 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
39 | 13, 38 | clwlkclwwlk 28345 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧
(2nd ‘𝑐)
∈ Word (Vtx‘𝐺)
∧ 2 ≤ (♯‘(2nd ‘𝑐))) → (∃𝑓 𝑓(ClWalks‘𝐺)(2nd ‘𝑐) ↔ ((lastS‘(2nd
‘𝑐)) =
((2nd ‘𝑐)‘0) ∧ ((2nd
‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1)) ∈ (ClWWalks‘𝐺)))) |
40 | 12, 16, 37, 39 | syl3anc 1369 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ)) → (∃𝑓 𝑓(ClWalks‘𝐺)(2nd ‘𝑐) ↔ ((lastS‘(2nd
‘𝑐)) =
((2nd ‘𝑐)‘0) ∧ ((2nd
‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1)) ∈ (ClWWalks‘𝐺)))) |
41 | 11, 40 | mpbid 231 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧
((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) ∧ ((2nd ‘𝑐)‘0) = ((2nd
‘𝑐)‘(♯‘(1st
‘𝑐))) ∧
(♯‘(1st ‘𝑐)) ∈ ℕ)) →
((lastS‘(2nd ‘𝑐)) = ((2nd ‘𝑐)‘0) ∧
((2nd ‘𝑐)
prefix ((♯‘(2nd ‘𝑐)) − 1)) ∈ (ClWWalks‘𝐺))) |
42 | 4, 41 | sylan2 592 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑐 ∈ 𝐶) → ((lastS‘(2nd
‘𝑐)) =
((2nd ‘𝑐)‘0) ∧ ((2nd
‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1)) ∈ (ClWWalks‘𝐺))) |
43 | 42 | simprd 495 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑐 ∈ 𝐶) → ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1)) ∈ (ClWWalks‘𝐺)) |
44 | | clwlkclwwlkf.f |
. 2
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
45 | 43, 44 | fmptd 6982 |
1
⊢ (𝐺 ∈ USPGraph → 𝐹:𝐶⟶(ClWWalks‘𝐺)) |