Step | Hyp | Ref
| Expression |
1 | | 1wlkn0 40825 |
. . 3
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃 ≠ ∅) |
2 | | wlkv 40815 |
. . . 4
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
3 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph ) → 𝐺 ∈ UPGraph
) |
4 | | simpl2 1058 |
. . . . . . . . 9
⊢ (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph ) → 𝐹 ∈ V) |
5 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph ) → 𝑃 ∈ V) |
6 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
7 | | eqid 2610 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
8 | 6, 7 | upgriswlk 40849 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
9 | 3, 4, 5, 8 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph ) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
10 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ≠ ∅) |
11 | | ffz0iswrd 13187 |
. . . . . . . . . . . . . 14
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → 𝑃 ∈ Word (Vtx‘𝐺)) |
12 | 11 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑃 ∈ Word (Vtx‘𝐺)) |
13 | 12 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ∈ Word (Vtx‘𝐺)) |
14 | | upgruhgr 25768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph
) |
15 | 7 | uhgrfun 25732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
16 | | funfn 5833 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
17 | 16 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Fun
(iEdg‘𝐺) →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
18 | 14, 15, 17 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
19 | 18 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
20 | | wrdsymbcl 13173 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
21 | 20 | ad4ant14 1285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
22 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) ∧
(𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
23 | 19, 21, 22 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
24 | | edgaval 25794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺 ∈ UPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
25 | 24 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (Edg‘𝐺) = ran (iEdg‘𝐺)) |
26 | 23, 25 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺)) |
27 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘(𝐹‘𝑖)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
28 | 27 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
29 | 26, 28 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
30 | 29 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) → (∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
31 | 30 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (𝐺 ∈ UPGraph → (∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
32 | 31 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (𝐺 ∈ UPGraph → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
33 | 32 | 3impia 1253 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐺 ∈ UPGraph → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
34 | 33 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
35 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(#‘𝐹) ∈
ℕ0) |
36 | | ffz0hash 13088 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (#‘𝑃) = ((#‘𝐹) + 1)) |
37 | 36 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) ∈
ℕ0 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (#‘𝑃) = ((#‘𝐹) + 1))) |
38 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) =
((#‘𝐹) + 1) →
((#‘𝑃) − 1) =
(((#‘𝐹) + 1) −
1)) |
39 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℂ) |
40 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℂ → (((#‘𝐹) + 1) − 1) = (#‘𝐹)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝐹) ∈
ℕ0 → (((#‘𝐹) + 1) − 1) = (#‘𝐹)) |
42 | 38, 41 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (#‘𝑃) = ((#‘𝐹) + 1)) → ((#‘𝑃) − 1) = (#‘𝐹)) |
43 | 42 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝑃) = ((#‘𝐹) + 1) → ((#‘𝑃) − 1) = (#‘𝐹))) |
44 | 37, 43 | syld 46 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) ∈
ℕ0 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((#‘𝑃) − 1) = (#‘𝐹))) |
45 | 35, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((#‘𝑃) − 1) = (#‘𝐹))) |
46 | 45 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → ((#‘𝑃) − 1) = (#‘𝐹)) |
47 | 46 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (0..^((#‘𝑃) − 1)) = (0..^(#‘𝐹))) |
48 | 47 | raleqdv 3121 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
49 | 48 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
51 | 34, 50 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
52 | 51 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
53 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
54 | 6, 53 | iswwlks 41039 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (WWalkS‘𝐺) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
55 | 10, 13, 52, 54 | syl3anbrc 1239 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ∈ (WWalkS‘𝐺)) |
56 | 55 | ex 449 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalkS‘𝐺))) |
57 | 56 | ex 449 |
. . . . . . . . 9
⊢ (𝐺 ∈ UPGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalkS‘𝐺)))) |
58 | 57 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph ) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalkS‘𝐺)))) |
59 | 9, 58 | sylbid 229 |
. . . . . . 7
⊢ (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph ) → (𝐹(1Walks‘𝐺)𝑃 → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalkS‘𝐺)))) |
60 | 59 | ex 449 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐺 ∈ UPGraph → (𝐹(1Walks‘𝐺)𝑃 → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalkS‘𝐺))))) |
61 | 60 | com23 84 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalkS‘𝐺))))) |
62 | 61 | com34 89 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 → (𝑃 ≠ ∅ → (𝐺 ∈ UPGraph → 𝑃 ∈ (WWalkS‘𝐺))))) |
63 | 2, 62 | mpcom 37 |
. . 3
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝑃 ≠ ∅ → (𝐺 ∈ UPGraph → 𝑃 ∈ (WWalkS‘𝐺)))) |
64 | 1, 63 | mpd 15 |
. 2
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → 𝑃 ∈ (WWalkS‘𝐺))) |
65 | 64 | com12 32 |
1
⊢ (𝐺 ∈ UPGraph → (𝐹(1Walks‘𝐺)𝑃 → 𝑃 ∈ (WWalkS‘𝐺))) |