Proof of Theorem uhgr1wlkspth
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | wlkOnprop 40866 |
. . . . 5
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
3 | | 3simpc 1053 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
4 | 3 | 3anim1i 1241 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
5 | 2, 4 | syl 17 |
. . . 4
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
6 | | simpl31 1135 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → 𝐹(1Walks‘𝐺)𝑃) |
7 | | uhgr1wlkspthlem1 40959 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (#‘𝐹) = 1) → Fun ◡𝐹) |
8 | 7 | expcom 450 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 1
→ (𝐹(1Walks‘𝐺)𝑃 → Fun ◡𝐹)) |
9 | 8 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(1Walks‘𝐺)𝑃 → Fun ◡𝐹)) |
10 | 9 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝐹(1Walks‘𝐺)𝑃 → ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → Fun ◡𝐹)) |
11 | 10 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → Fun ◡𝐹)) |
12 | 11 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → Fun ◡𝐹)) |
13 | 12 | imp 444 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → Fun ◡𝐹) |
14 | 1 | 1vgrex 25679 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (Vtx‘𝐺) → 𝐺 ∈ V) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) → 𝐺 ∈ V) |
16 | 15 | anim1i 590 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐺 ∈ V ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
17 | | 3anass 1035 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ↔ (𝐺 ∈ V ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
18 | 16, 17 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
19 | | isTrl 40904 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))) |
21 | 20 | 3adant3 1074 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))) |
23 | 6, 13, 22 | mpbir2and 959 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → 𝐹(TrailS‘𝐺)𝑃) |
24 | | 3simpc 1053 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → ((#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) |
25 | 24 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → ((#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) |
26 | | 3simpc 1053 |
. . . . . . . . . . 11
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) |
27 | 26 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) |
28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) |
29 | | uhgr1wlkspthlem2 40960 |
. . . . . . . . 9
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ ((#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → Fun ◡𝑃) |
30 | 6, 25, 28, 29 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → Fun ◡𝑃) |
31 | | wlkv 40815 |
. . . . . . . . . . . 12
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
32 | 31 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
33 | 32 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
34 | | issPth 40930 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
36 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
37 | 23, 30, 36 | mpbir2and 959 |
. . . . . . 7
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → 𝐹(SPathS‘𝐺)𝑃) |
38 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝐹(SPathS‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ↔ (𝐹(SPathS‘𝐺)𝑃 ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
39 | 37, 28, 38 | sylanbrc 695 |
. . . . . 6
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → (𝐹(SPathS‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) |
40 | | 3simpa 1051 |
. . . . . . . 8
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
41 | 40 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
42 | 1 | isspthonpth-av 40955 |
. . . . . . 7
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(SPathS‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
43 | 41, 42 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(SPathS‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
44 | 39, 43 | mpbird 246 |
. . . . 5
⊢ ((((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ (𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵)) → 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃) |
45 | 44 | ex 449 |
. . . 4
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) |
46 | 5, 45 | syl 17 |
. . 3
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) |
47 | 46 | com12 32 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) |
48 | | spthonpthon 40957 |
. . 3
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃) |
49 | | pthontrlon 40953 |
. . 3
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃) |
50 | | trlsonwlkon 40917 |
. . 3
⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃) |
51 | 48, 49, 50 | 3syl 18 |
. 2
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃) |
52 | 47, 51 | impbid1 214 |
1
⊢ ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) |