Step | Hyp | Ref
| Expression |
1 | | df-cycl 26041 |
. . . 4
⊢ Cycles =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Paths 𝑒)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) |
2 | 1 | brovmpt2ex 7236 |
. . 3
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | | iscycl 26153 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
4 | | pthistrl 26102 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → 𝐹(𝑉 Trails 𝐸)𝑃) |
5 | | trliswlk 26069 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Trails 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
6 | | 2mwlk 26049 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
7 | | lennncl 13180 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝐹 ≠ ∅) → (#‘𝐹) ∈
ℕ) |
8 | | df-f1 5809 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ↔ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡𝑃)) |
9 | | nnne0 10930 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) ∈
ℕ → (#‘𝐹)
≠ 0) |
10 | 9 | necomd 2837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) ∈
ℕ → 0 ≠ (#‘𝐹)) |
11 | 10 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝐹) ∈
ℕ → ¬ 0 = (#‘𝐹)) |
12 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝐹) ∈
ℕ ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ¬ 0 = (#‘𝐹)) |
13 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐹) ∈
ℕ ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 𝑃:(0...(#‘𝐹))–1-1→𝑉) |
14 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) ∈
ℕ → (#‘𝐹)
∈ ℕ0) |
15 | | 0elfz 12305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) ∈
ℕ0 → 0 ∈ (0...(#‘𝐹))) |
16 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈
ℕ0) |
17 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℝ) |
18 | 17 | leidd 10473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ≤ (#‘𝐹)) |
19 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) ∈
(0...(#‘𝐹)) ↔
((#‘𝐹) ∈
ℕ0 ∧ (#‘𝐹) ∈ ℕ0 ∧
(#‘𝐹) ≤
(#‘𝐹))) |
20 | 16, 16, 18, 19 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ (0...(#‘𝐹))) |
21 | 15, 20 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) ∈
ℕ0 → (0 ∈ (0...(#‘𝐹)) ∧ (#‘𝐹) ∈ (0...(#‘𝐹)))) |
22 | 14, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) ∈
ℕ → (0 ∈ (0...(#‘𝐹)) ∧ (#‘𝐹) ∈ (0...(#‘𝐹)))) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐹) ∈
ℕ ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (0 ∈ (0...(#‘𝐹)) ∧ (#‘𝐹) ∈ (0...(#‘𝐹)))) |
24 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (0 ∈ (0...(#‘𝐹)) ∧ (#‘𝐹) ∈ (0...(#‘𝐹)))) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ 0 = (#‘𝐹))) |
25 | 13, 23, 24 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝐹) ∈
ℕ ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ 0 = (#‘𝐹))) |
26 | 12, 25 | mtbird 314 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝐹) ∈
ℕ ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ¬ (𝑃‘0) = (𝑃‘(#‘𝐹))) |
27 | 26 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((#‘𝐹) ∈ ℕ → ¬ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
28 | 8, 27 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡𝑃) → ((#‘𝐹) ∈ ℕ → ¬ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
29 | 28 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑃 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝐹) ∈ ℕ → ¬ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
30 | 29 | com13 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) ∈
ℕ → (𝑃:(0...(#‘𝐹))⟶𝑉 → (Fun ◡𝑃 → ¬ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
31 | 30 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (Fun ◡𝑃 → ¬ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
32 | 31 | con2d 128 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → ¬ Fun ◡𝑃)) |
33 | 32 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) ∈
ℕ → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → ¬ Fun ◡𝑃))) |
34 | 33 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
ℕ → ((𝑃‘0)
= (𝑃‘(#‘𝐹)) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ¬ Fun ◡𝑃))) |
35 | 7, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝐹 ≠ ∅) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ¬ Fun ◡𝑃))) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word dom 𝐸 → (𝐹 ≠ ∅ → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ¬ Fun ◡𝑃)))) |
37 | 36 | com24 93 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐹 ≠ ∅ → ¬ Fun ◡𝑃)))) |
38 | 37 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐹 ≠ ∅ → ¬ Fun ◡𝑃))) |
39 | 4, 5, 6, 38 | 4syl 19 |
. . . . . . . . . . 11
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐹 ≠ ∅ → ¬ Fun ◡𝑃))) |
40 | 39 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐹 ≠ ∅ → ¬ Fun ◡𝑃)) |
41 | 40 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (𝐹 ≠ ∅ → ¬ Fun ◡𝑃)) |
42 | 41 | imp 444 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) ∧ 𝐹 ≠ ∅) → ¬ Fun ◡𝑃) |
43 | 42 | intnand 953 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) ∧ 𝐹 ≠ ∅) → ¬ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) |
44 | | isspth 26099 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
45 | 44 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
46 | 45 | adantr 480 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) ∧ 𝐹 ≠ ∅) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
47 | 43, 46 | mtbird 314 |
. . . . . 6
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) ∧ 𝐹 ≠ ∅) → ¬ 𝐹(𝑉 SPaths 𝐸)𝑃) |
48 | 47 | ex 449 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (𝐹 ≠ ∅ → ¬ 𝐹(𝑉 SPaths 𝐸)𝑃)) |
49 | 48 | ex 449 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐹 ≠ ∅ → ¬ 𝐹(𝑉 SPaths 𝐸)𝑃))) |
50 | 3, 49 | sylbid 229 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝐹 ≠ ∅ → ¬ 𝐹(𝑉 SPaths 𝐸)𝑃))) |
51 | 2, 50 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝐹 ≠ ∅ → ¬ 𝐹(𝑉 SPaths 𝐸)𝑃)) |
52 | 51 | com12 32 |
1
⊢ (𝐹 ≠ ∅ → (𝐹(𝑉 Cycles 𝐸)𝑃 → ¬ 𝐹(𝑉 SPaths 𝐸)𝑃)) |