Step | Hyp | Ref
| Expression |
1 | | clwlksfclwwlk.1 |
. . 3
⊢ 𝐴 = (1st ‘𝑐) |
2 | | clwlksfclwwlk.2 |
. . 3
⊢ 𝐵 = (2nd ‘𝑐) |
3 | | clwlksfclwwlk.c |
. . 3
⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} |
4 | | clwlksfclwwlk.f |
. . 3
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) |
5 | 1, 2, 3, 4 | clwlksfclwwlk 26962 |
. 2
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺)) |
6 | | eqid 2622 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
7 | 6 | clwwlknbp 26885 |
. . . . 5
⊢ (𝑤 ∈ (𝑁 ClWWalksN 𝐺) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) |
8 | 7 | adantl 482 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) |
9 | | prmnn 15388 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
10 | 9 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → 𝑁 ∈ ℕ) |
11 | | isclwwlksn 26882 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑤 ∈ (𝑁 ClWWalksN 𝐺) ↔ (𝑤 ∈ (ClWWalks‘𝐺) ∧ (#‘𝑤) = 𝑁))) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ (𝑁 ClWWalksN 𝐺) ↔ (𝑤 ∈ (ClWWalks‘𝐺) ∧ (#‘𝑤) = 𝑁))) |
13 | | fusgrusgr 26214 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph
) |
14 | | usgruspgr 26073 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph
) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USPGraph
) |
16 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USPGraph
) |
17 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → 𝐺 ∈ USPGraph ) |
18 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → 𝑤 ∈ Word (Vtx‘𝐺)) |
19 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 𝑁 → ((#‘𝑤) ∈ ℙ ↔ 𝑁 ∈
ℙ)) |
20 | | prmnn 15388 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) ∈
ℙ → (#‘𝑤)
∈ ℕ) |
21 | 20 | nnge1d 11063 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) ∈
ℙ → 1 ≤ (#‘𝑤)) |
22 | 19, 21 | syl6bir 244 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑤) = 𝑁 → (𝑁 ∈ ℙ → 1 ≤ (#‘𝑤))) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ ℙ → 1 ≤ (#‘𝑤))) |
24 | 23 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℙ → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → 1 ≤ (#‘𝑤))) |
25 | 24 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → 1 ≤ (#‘𝑤))) |
26 | 25 | imp 445 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → 1 ≤ (#‘𝑤)) |
27 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
28 | 6, 27 | clwlkclwwlk2 26904 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 𝑤 ∈ (ClWWalks‘𝐺))) |
29 | 17, 18, 26, 28 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 𝑤 ∈ (ClWWalks‘𝐺))) |
30 | 29 | bicomd 213 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ (ClWWalks‘𝐺) ↔ ∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉))) |
31 | 30 | anbi1d 741 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → ((𝑤 ∈ (ClWWalks‘𝐺) ∧ (#‘𝑤) = 𝑁) ↔ (∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ∧ (#‘𝑤) = 𝑁))) |
32 | 12, 31 | bitrd 268 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ (𝑁 ClWWalksN 𝐺) ↔ (∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ∧ (#‘𝑤) = 𝑁))) |
33 | | df-br 4654 |
. . . . . . . . 9
⊢ (𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) |
34 | | simpl 473 |
. . . . . . . . . . . . 13
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) |
35 | 9 | nnge1d 11063 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℙ → 1 ≤
𝑁) |
36 | 35 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → 1 ≤ 𝑁) |
37 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑤) = 𝑁 → (1 ≤ (#‘𝑤) ↔ 1 ≤ 𝑁)) |
38 | 37 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (1 ≤ (#‘𝑤) ↔ 1 ≤ 𝑁)) |
39 | 36, 38 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → 1 ≤ (#‘𝑤)) |
40 | 18, 39 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤))) |
41 | | clwlkwlk 26671 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (Walks‘𝐺)) |
42 | | wlklenvclwlk 26551 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(Walks‘𝐺) →
(#‘𝑓) =
(#‘𝑤))) |
43 | 40, 41, 42 | syl2im 40 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) =
(#‘𝑤))) |
44 | 43 | impcom 446 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → (#‘𝑓) = (#‘𝑤)) |
45 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑓 ∈ V |
46 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ++ 〈“(𝑤‘0)”〉) ∈
V |
47 | 45, 46 | op1st 7176 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = 𝑓 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = 𝑓) |
49 | 48 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= (#‘𝑓)) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) →
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(#‘𝑓)) |
51 | | eqcom 2629 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) = 𝑁 ↔ 𝑁 = (#‘𝑤)) |
52 | 51 | biimpi 206 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 𝑁 → 𝑁 = (#‘𝑤)) |
53 | 52 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → 𝑁 = (#‘𝑤)) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → 𝑁 = (#‘𝑤)) |
55 | 44, 50, 54 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) →
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) = 𝑁) |
56 | 1 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
⊢
(#‘𝐴) =
(#‘(1st ‘𝑐)) |
57 | 56 | eqeq1i 2627 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐴) = 𝑁 ↔ (#‘(1st
‘𝑐)) = 𝑁) |
58 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(1st ‘𝑐) =
(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
59 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(#‘(1st ‘𝑐)) = (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
60 | 59 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘(1st ‘𝑐)) = 𝑁 ↔ (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= 𝑁)) |
61 | 57, 60 | syl5bb 272 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘𝐴) = 𝑁 ↔ (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= 𝑁)) |
62 | 61, 3 | elrab2 3366 |
. . . . . . . . . . . . 13
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ↔
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) = 𝑁)) |
63 | 34, 55, 62 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ 𝐶) |
64 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
(#‘𝑓) =
(#‘𝑤)) |
65 | 64 | opeq2d 4409 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
〈0, (#‘𝑓)〉
= 〈0, (#‘𝑤)〉) |
66 | 65 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)
= ((𝑤 ++
〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉)) |
67 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)) |
68 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) =
(#‘𝑤))) |
69 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 = (#‘𝑤) → ((#‘𝑓) = 𝑁 ↔ (#‘𝑓) = (#‘𝑤))) |
70 | 69 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑤) = 𝑁 → ((#‘𝑓) = 𝑁 ↔ (#‘𝑓) = (#‘𝑤))) |
71 | 70 | imbi2d 330 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑤) = 𝑁 → ((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) = 𝑁) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) =
(#‘𝑤)))) |
72 | 71 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → ((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) = 𝑁) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) =
(#‘𝑤)))) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → ((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) = 𝑁) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) =
(#‘𝑤)))) |
74 | 68, 73 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
(#‘𝑓) = 𝑁)) |
75 | 74 | imp 445 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
(#‘𝑓) = 𝑁) |
76 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = 𝑓) |
77 | 76 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(#‘𝑓)) |
78 | 59, 77 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(#‘(1st ‘𝑐)) = (#‘𝑓)) |
79 | 78 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘(1st ‘𝑐)) = 𝑁 ↔ (#‘𝑓) = 𝑁)) |
80 | 57, 79 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘𝐴) = 𝑁 ↔ (#‘𝑓) = 𝑁)) |
81 | 80, 3 | elrab2 3366 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ↔
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ (#‘𝑓) = 𝑁)) |
82 | 67, 75, 81 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶) |
83 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)
∈ V |
84 | 56 | opeq2i 4406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 〈0,
(#‘𝐴)〉 =
〈0, (#‘(1st ‘𝑐))〉 |
85 | 2, 84 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 substr 〈0, (#‘𝐴)〉) = ((2nd
‘𝑐) substr 〈0,
(#‘(1st ‘𝑐))〉) |
86 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(2nd ‘𝑐) =
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
87 | 59 | opeq2d 4409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → 〈0,
(#‘(1st ‘𝑐))〉 = 〈0, (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉) |
88 | 86, 87 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
substr 〈0, (#‘(1st ‘𝑐))〉) = ((2nd
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)
substr 〈0, (#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉)) |
89 | 45, 46 | op2nd 7177 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = (𝑤 ++ 〈“(𝑤‘0)”〉) |
90 | 47 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(#‘𝑓) |
91 | 90 | opeq2i 4406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 〈0,
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉 =
〈0, (#‘𝑓)〉 |
92 | 89, 91 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) substr
〈0, (#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉) =
((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉) |
93 | 88, 92 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
substr 〈0, (#‘(1st ‘𝑐))〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑓)〉)) |
94 | 85, 93 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝐵 substr 〈0, (#‘𝐴)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑓)〉)) |
95 | 94, 4 | fvmptg 6280 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ∧ ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)
∈ V) → (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)) |
96 | 82, 83, 95 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
(𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)) |
97 | 40 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
(𝑤 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(#‘𝑤))) |
98 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → 𝑤 ∈ Word (Vtx‘𝐺)) |
99 | | wrdsymb1 13342 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → (𝑤‘0) ∈ (Vtx‘𝐺)) |
100 | 99 | s1cld 13383 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → 〈“(𝑤‘0)”〉 ∈
Word (Vtx‘𝐺)) |
101 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → (#‘𝑤) = (#‘𝑤)) |
102 | | swrdccatid 13497 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑤‘0)”〉 ∈
Word (Vtx‘𝐺) ∧
(#‘𝑤) =
(#‘𝑤)) → ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑤)〉)
= 𝑤) |
103 | 98, 100, 101, 102 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉) = 𝑤) |
104 | 103 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑤)) → 𝑤 = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉)) |
105 | 97, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
𝑤 = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉)) |
106 | 66, 96, 105 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺)) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
107 | 106 | ex 450 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
108 | 107 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
109 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝐹‘𝑐) = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
110 | 109 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝑤 = (𝐹‘𝑐) ↔ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
111 | 110 | imbi2d 330 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
112 | 111 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
113 | 108, 112 | mpbird 247 |
. . . . . . . . . . . 12
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) ∧ 𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ 𝑤 = (𝐹‘𝑐))) |
114 | 63, 113 | rspcimedv 3311 |
. . . . . . . . . . 11
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
∧ ((𝐺 ∈ FinUSGraph
∧ 𝑁 ∈ ℙ)
∧ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁))) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
115 | 114 | ex 450 |
. . . . . . . . . 10
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (ClWalks‘𝐺)
→ (((𝐺 ∈
FinUSGraph ∧ 𝑁 ∈
ℙ) ∧ (𝑤 ∈
Word (Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)))) |
116 | 115 | pm2.43b 55 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈
(ClWalks‘𝐺) →
∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
117 | 33, 116 | syl5bi 232 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
118 | 117 | exlimdv 1861 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
119 | 118 | adantrd 484 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → ((∃𝑓 𝑓(ClWalks‘𝐺)(𝑤 ++ 〈“(𝑤‘0)”〉) ∧ (#‘𝑤) = 𝑁) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
120 | 32, 119 | sylbid 230 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ (𝑁 ClWWalksN 𝐺) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
121 | 120 | impancom 456 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
122 | 8, 121 | mpd 15 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
123 | 122 | ralrimiva 2966 |
. 2
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
∀𝑤 ∈ (𝑁 ClWWalksN 𝐺)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
124 | | dffo3 6374 |
. 2
⊢ (𝐹:𝐶–onto→(𝑁 ClWWalksN 𝐺) ↔ (𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺) ∧ ∀𝑤 ∈ (𝑁 ClWWalksN 𝐺)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
125 | 5, 123, 124 | sylanbrc 698 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–onto→(𝑁 ClWWalksN 𝐺)) |