Step | Hyp | Ref
| Expression |
1 | | iswspthn 41047 |
. . 3
⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ (𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊)) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ (𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊))) |
3 | | wwlksnwwlksnon.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
4 | 3 | wwlksnwwlksnon 41121 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WWalkSN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |
5 | 4 | anbi1d 737 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊) ↔ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊))) |
6 | | r19.41vv 3072 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊) ↔ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊)) |
7 | 5, 6 | syl6bbr 277 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊))) |
8 | | 3anass 1035 |
. . . . . . . 8
⊢ ((𝑓(SPathS‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏) ↔ (𝑓(SPathS‘𝐺)𝑊 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((𝑓(SPathS‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏) ↔ (𝑓(SPathS‘𝐺)𝑊 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
10 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
11 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
12 | 11 | jctl 562 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) → (𝑓 ∈ V ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |
13 | 3 | isspthonpth-av 40955 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑓 ∈ V ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) → (𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊 ↔ (𝑓(SPathS‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
14 | 10, 12, 13 | syl2an 493 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊 ↔ (𝑓(SPathS‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
15 | | sPthis1wlk 40934 |
. . . . . . . . . 10
⊢ (𝑓(SPathS‘𝐺)𝑊 → 𝑓(1Walks‘𝐺)𝑊) |
16 | | 1wlklenvm1 40826 |
. . . . . . . . . 10
⊢ (𝑓(1Walks‘𝐺)𝑊 → (#‘𝑓) = ((#‘𝑊) − 1)) |
17 | 3 | wwlknon 41053 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏))) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏))) |
19 | | simpl2 1058 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘0) = 𝑎) |
20 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑓) =
((#‘𝑊) − 1))
→ (#‘𝑓) =
((#‘𝑊) −
1)) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (#‘𝑓) =
((#‘𝑊) −
1)) |
22 | | wwlknbp2 41063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) |
23 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
24 | 23 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) − 1) = ((𝑁 + 1) − 1)) |
25 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
26 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑓) =
((#‘𝑊) − 1))
→ ((𝑁 + 1) − 1)
= 𝑁) |
29 | 24, 28 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ ((#‘𝑊) −
1) = 𝑁) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1))
→ ((#‘𝑊) −
1) = 𝑁)) |
31 | 22, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1))
→ ((#‘𝑊) −
1) = 𝑁)) |
32 | 31 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1))
→ ((#‘𝑊) −
1) = 𝑁)) |
33 | 32 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ ((#‘𝑊) −
1) = 𝑁) |
34 | 21, 33 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (#‘𝑓) = 𝑁) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘(#‘𝑓)) = (𝑊‘𝑁)) |
36 | | simpl3 1059 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘𝑁) = 𝑏) |
37 | 35, 36 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘(#‘𝑓)) = 𝑏) |
38 | 19, 37 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)) |
39 | 38 | exp32 629 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → (𝑁 ∈ ℕ0 →
((#‘𝑓) =
((#‘𝑊) − 1)
→ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
40 | 39 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
43 | 18, 42 | sylbid 229 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
44 | 43 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
45 | 44 | com12 32 |
. . . . . . . . . 10
⊢
((#‘𝑓) =
((#‘𝑊) − 1)
→ ((((𝑁 ∈
ℕ0 ∧ 𝐺
∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
46 | 15, 16, 45 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑓(SPathS‘𝐺)𝑊 → ((((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
47 | 46 | com12 32 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(SPathS‘𝐺)𝑊 → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
48 | 47 | pm4.71d 664 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(SPathS‘𝐺)𝑊 ↔ (𝑓(SPathS‘𝐺)𝑊 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
49 | 9, 14, 48 | 3bitr4rd 300 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(SPathS‘𝐺)𝑊 ↔ 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊)) |
50 | 49 | exbidv 1837 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (∃𝑓 𝑓(SPathS‘𝐺)𝑊 ↔ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊)) |
51 | 50 | pm5.32da 671 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊) ↔ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊))) |
52 | 3 | wspthnon 41054 |
. . . . 5
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊))) |
53 | 52 | adantl 481 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊))) |
54 | 51, 53 | bitr4d 270 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊) ↔ 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏))) |
55 | 54 | 2rexbidva 3038 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏))) |
56 | 2, 7, 55 | 3bitrd 293 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏))) |