| Step | Hyp | Ref
| Expression |
| 1 | | clwlkclwwlkf.c |
. . 3
⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤
(♯‘(1st ‘𝑤))} |
| 2 | | clwlkclwwlkf.f |
. . 3
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ ((2nd ‘𝑐) prefix
((♯‘(2nd ‘𝑐)) − 1))) |
| 3 | 1, 2 | clwlkclwwlkf 30027 |
. 2
⊢ (𝐺 ∈ USPGraph → 𝐹:𝐶⟶(ClWWalks‘𝐺)) |
| 4 | | clwwlkgt0 30005 |
. . . . . 6
⊢ (𝑤 ∈ (ClWWalks‘𝐺) → 0 <
(♯‘𝑤)) |
| 5 | | eqid 2737 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 6 | 5 | clwwlkbp 30004 |
. . . . . . 7
⊢ (𝑤 ∈ (ClWWalks‘𝐺) → (𝐺 ∈ V ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑤 ≠ ∅)) |
| 7 | | lencl 14571 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (♯‘𝑤) ∈
ℕ0) |
| 8 | 7 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (♯‘𝑤) ∈
ℤ) |
| 9 | | zgt0ge1 12672 |
. . . . . . . . . . 11
⊢
((♯‘𝑤)
∈ ℤ → (0 < (♯‘𝑤) ↔ 1 ≤ (♯‘𝑤))) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (0 <
(♯‘𝑤) ↔ 1
≤ (♯‘𝑤))) |
| 11 | 10 | biimpd 229 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (0 <
(♯‘𝑤) → 1
≤ (♯‘𝑤))) |
| 12 | 11 | anc2li 555 |
. . . . . . . 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 481 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (ClWWalks‘𝐺)) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (♯‘𝑤))) |
| 17 | | eqid 2737 |
. . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 18 | 5, 17 | clwlkclwwlk2 30022 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 𝑤 ∈ (ClWWalks‘𝐺))) |
| 19 | | df-br 5144 |
. . . . . . . . . 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 482 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)) |
| 23 | 1 | clwlkclwwlkfolem 30026 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶) |
| 24 | 20, 21, 22, 23 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶) |
| 25 | 23 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶) |
| 26 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) − 1)) ∈
V |
| 27 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(2nd ‘𝑐) =
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
| 28 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(♯‘(2nd ‘𝑐)) = (♯‘(2nd
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
| 29 | 28 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((♯‘(2nd ‘𝑐)) − 1) =
((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) −
1)) |
| 30 | 27, 29 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
prefix ((♯‘(2nd ‘𝑐)) − 1)) = ((2nd
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)
prefix ((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) −
1))) |
| 31 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑓 ∈ V |
| 32 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ++ 〈“(𝑤‘0)”〉) ∈
V |
| 33 | 31, 32 | op2nd 8023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = (𝑤 ++ 〈“(𝑤‘0)”〉) |
| 34 | 33 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) |
| 35 | 34 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) − 1) =
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1) |
| 36 | 33, 35 | oveq12i 7443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) prefix
((♯‘(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) − 1)) =
((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1)) |
| 37 | 30, 36 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
prefix ((♯‘(2nd ‘𝑐)) − 1)) = ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1))) |
| 38 | 37, 2 | fvmptg 7014 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ∧ ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) − 1)) ∈
V) → (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1))) |
| 39 | 25, 26, 38 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
((♯‘(𝑤 ++
〈“(𝑤‘0)”〉)) −
1))) |
| 40 | | wrdlenccats1lenm1 14660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → ((♯‘(𝑤 ++ 〈“(𝑤‘0)”〉)) −
1) = (♯‘𝑤)) |
| 41 | 40 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ ((♯‘(𝑤
++ 〈“(𝑤‘0)”〉)) − 1) =
(♯‘𝑤)) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 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 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) |
| 45 | | wrdsymb1 14591 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(𝑤‘0) ∈
(Vtx‘𝐺)) |
| 46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (𝑤‘0) ∈
(Vtx‘𝐺)) |
| 47 | 46 | s1cld 14641 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 〈“(𝑤‘0)”〉 ∈ Word
(Vtx‘𝐺)) |
| 48 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ (♯‘𝑤) =
(♯‘𝑤)) |
| 49 | | pfxccatid 14779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑤‘0)”〉 ∈
Word (Vtx‘𝐺) ∧
(♯‘𝑤) =
(♯‘𝑤)) →
((𝑤 ++ 〈“(𝑤‘0)”〉) prefix
(♯‘𝑤)) = 𝑤) |
| 50 | 43, 47, 48, 49 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ ((𝑤 ++
〈“(𝑤‘0)”〉) prefix
(♯‘𝑤)) = 𝑤) |
| 51 | 39, 42, 50 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) ∧
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺))
→ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
| 52 | 51 | ex 412 |
. . . . . . . . . . . . . . . 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 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝐹‘𝑐) = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
| 56 | 55 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝑤 = (𝐹‘𝑐) ↔ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
| 57 | 56 | imbi2d 340 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
| 58 | 57 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) ∧
𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
| 59 | 54, 58 | mpbird 257 |
. . . . . . . . . . . . 13
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) ∧
𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐))) |
| 60 | 24, 59 | rspcimedv 3613 |
. . . . . . . . . . . 12
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤))) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ∃𝑐 ∈
𝐶 𝑤 = (𝐹‘𝑐))) |
| 61 | 60 | ex 412 |
. . . . . . . . . . 11
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ((𝐺 ∈ USPGraph
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ∃𝑐 ∈
𝐶 𝑤 = (𝐹‘𝑐)))) |
| 62 | 61 | pm2.43b 55 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ ∃𝑐 ∈
𝐶 𝑤 = (𝐹‘𝑐))) |
| 63 | 19, 62 | biimtrid 242 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
| 64 | 63 | exlimdv 1933 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑤)) →
(∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
| 65 | 18, 64 | sylbird 260 |
. . . . . . 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 406 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (ClWWalks‘𝐺)) → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (♯‘𝑤)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
| 69 | 16, 68 | mpd 15 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (ClWWalks‘𝐺)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
| 70 | 69 | ralrimiva 3146 |
. 2
⊢ (𝐺 ∈ USPGraph →
∀𝑤 ∈
(ClWWalks‘𝐺)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
| 71 | | dffo3 7122 |
. 2
⊢ (𝐹:𝐶–onto→(ClWWalks‘𝐺) ↔ (𝐹:𝐶⟶(ClWWalks‘𝐺) ∧ ∀𝑤 ∈ (ClWWalks‘𝐺)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
| 72 | 3, 70, 71 | sylanbrc 583 |
1
⊢ (𝐺 ∈ USPGraph → 𝐹:𝐶–onto→(ClWWalks‘𝐺)) |