Step | Hyp | Ref
| Expression |
1 | | clwlkclwwlkf.c |
. . 3
⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} |
2 | | clwlkclwwlkf.f |
. . 3
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
3 | 1, 2 | clwlkclwwlkf 27957 |
. 2
⊢ (𝐺 ∈ USPGraph → 𝐹:𝐶⟶(ClWWalks‘𝐺)) |
4 | | clwwlkgt0 27935 |
. . . . . 6
⊢ (𝑤 ∈ (ClWWalks‘𝐺) → 0 <
(♯‘𝑤)) |
5 | | eqid 2739 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | 5 | clwwlkbp 27934 |
. . . . . . 7
⊢ (𝑤 ∈ (ClWWalks‘𝐺) → (𝐺 ∈ V ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑤 ≠ ∅)) |
7 | | lencl 13986 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (♯‘𝑤) ∈
ℕ0) |
8 | 7 | nn0zd 12178 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (♯‘𝑤) ∈
ℤ) |
9 | | zgt0ge1 12129 |
. . . . . . . . . . 11
⊢
((♯‘𝑤)
∈ ℤ → (0 < (♯‘𝑤) ↔ 1 ≤ (♯‘𝑤))) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (0 <
(♯‘𝑤) ↔ 1
≤ (♯‘𝑤))) |
11 | 10 | biimpd 232 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (0 <
(♯‘𝑤) → 1
≤ (♯‘𝑤))) |
12 | 11 | anc2li 559 |
. . . . . . . 8
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (0 <
(♯‘𝑤) →
(𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)))) |
13 | 12 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑤 ≠ ∅) → (0 <
(♯‘𝑤) →
(𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)))) |
14 | 6, 13 | syl 17 |
. . . . . 6
⊢ (𝑤 ∈ (ClWWalks‘𝐺) → (0 <
(♯‘𝑤) →
(𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)))) |
15 | 4, 14 | mpd 15 |
. . . . 5
⊢ (𝑤 ∈ (ClWWalks‘𝐺) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (♯‘𝑤))) |
16 | 15 | adantl 485 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (ClWWalks‘𝐺)) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (♯‘𝑤))) |
17 | | eqid 2739 |
. . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
18 | 5, 17 | clwlkclwwlk2 27952 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 𝑤 ∈ (ClWWalks‘𝐺))) |
19 | | df-br 5041 |
. . . . . . . . . 10
⊢ (𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) |
20 | | simpr2 1196 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
𝑤 ∈ Word
(Vtx‘𝐺)) |
21 | | simpr3 1197 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
1 ≤ (♯‘𝑤)) |
22 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)) |
23 | 1 | clwlkclwwlkfolem 27956 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶) |
24 | 20, 21, 22, 23 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶) |
25 | 23 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶) |
26 | | ovex 7215 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) − 1)) ∈
V |
27 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(2nd ‘𝑐) =
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
28 | | 2fveq3 6691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(♯‘(2nd ‘𝑐)) = (♯‘(2nd
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
29 | 28 | oveq1d 7197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((♯‘(2nd ‘𝑐)) − 1) =
((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) −
1)) |
30 | 27, 29 | oveq12d 7200 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
prefix ((♯‘(2nd ‘𝑐)) − 1)) = ((2nd
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)
prefix ((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) −
1))) |
31 | | vex 3404 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑓 ∈ V |
32 | | ovex 7215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ++ 〈“(𝑤‘0)”〉) ∈
V |
33 | 31, 32 | op2nd 7735 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = (𝑤 ++ 〈“(𝑤‘0)”〉) |
34 | 33 | fveq2i 6689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) |
35 | 34 | oveq1i 7192 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) − 1) =
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1) |
36 | 33, 35 | oveq12i 7194 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) prefix
((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) − 1)) =
((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1)) |
37 | 30, 36 | eqtrdi 2790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
prefix ((♯‘(2nd ‘𝑐)) − 1)) = ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1))) |
38 | 37, 2 | fvmptg 6785 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ∧ ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) − 1)) ∈
V) → (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1))) |
39 | 25, 26, 38 | sylancl 589 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1))) |
40 | | wrdlenccats1lenm1 14077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → ((♯‘(𝑤 ++ 〈“(𝑤‘0)”〉)) −
1) = (♯‘𝑤)) |
41 | 40 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ ((♯‘(𝑤
++ 〈“(𝑤‘0)”〉)) − 1) =
(♯‘𝑤)) |
42 | 41 | oveq2d 7198 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ ((𝑤 ++
〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) − 1)) =
((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
(♯‘𝑤))) |
43 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 𝑤 ∈ Word
(Vtx‘𝐺)) |
44 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) |
45 | | wrdsymb1 14006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(𝑤‘0) ∈
(Vtx‘𝐺)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (𝑤‘0) ∈
(Vtx‘𝐺)) |
47 | 46 | s1cld 14058 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 〈“(𝑤‘0)”〉 ∈ Word
(Vtx‘𝐺)) |
48 | | eqidd 2740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (♯‘𝑤) =
(♯‘𝑤)) |
49 | | pfxccatid 14204 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑤‘0)”〉 ∈
Word (Vtx‘𝐺) ∧
(♯‘𝑤) =
(♯‘𝑤)) →
((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
(♯‘𝑤)) = 𝑤) |
50 | 43, 47, 48, 49 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ ((𝑤 ++
〈“(𝑤‘0)”〉) prefix
(♯‘𝑤)) = 𝑤) |
51 | 39, 42, 50 | 3eqtrrd 2779 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
52 | 51 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
53 | 52 | 3adant1 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
54 | 53 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) ∧
𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
55 | | fveq2 6686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝐹‘𝑐) = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
56 | 55 | eqeq2d 2750 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝑤 = (𝐹‘𝑐) ↔ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
57 | 56 | imbi2d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
58 | 57 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) ∧
𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
59 | 54, 58 | mpbird 260 |
. . . . . . . . . . . . 13
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) ∧
𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐))) |
60 | 24, 59 | rspcimedv 3520 |
. . . . . . . . . . . 12
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ∃𝑐 ∈
𝐶 𝑤 = (𝐹‘𝑐))) |
61 | 60 | ex 416 |
. . . . . . . . . . 11
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ((𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ∃𝑐 ∈
𝐶 𝑤 = (𝐹‘𝑐)))) |
62 | 61 | pm2.43b 55 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ∃𝑐 ∈
𝐶 𝑤 = (𝐹‘𝑐))) |
63 | 19, 62 | syl5bi 245 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
64 | 63 | exlimdv 1940 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
65 | 18, 64 | sylbird 263 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(𝑤 ∈
(ClWWalks‘𝐺) →
∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
66 | 65 | 3expib 1123 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(𝑤 ∈
(ClWWalks‘𝐺) →
∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)))) |
67 | 66 | com23 86 |
. . . . 5
⊢ (𝐺 ∈ USPGraph → (𝑤 ∈ (ClWWalks‘𝐺) → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (♯‘𝑤)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)))) |
68 | 67 | imp 410 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (ClWWalks‘𝐺)) → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (♯‘𝑤)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
69 | 16, 68 | mpd 15 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (ClWWalks‘𝐺)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
70 | 69 | ralrimiva 3097 |
. 2
⊢ (𝐺 ∈ USPGraph →
∀𝑤 ∈
(ClWWalks‘𝐺)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
71 | | dffo3 6890 |
. 2
⊢ (𝐹:𝐶–onto→(ClWWalks‘𝐺) ↔ (𝐹:𝐶⟶(ClWWalks‘𝐺) ∧ ∀𝑤 ∈ (ClWWalks‘𝐺)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
72 | 3, 70, 71 | sylanbrc 586 |
1
⊢ (𝐺 ∈ USPGraph → 𝐹:𝐶–onto→(ClWWalks‘𝐺)) |