Step | Hyp | Ref
| Expression |
1 | | cyclispth 26157 |
. . . 4
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Paths 𝐸)𝑃) |
2 | | pthistrl 26102 |
. . . . 5
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → 𝐹(𝑉 Trails 𝐸)𝑃) |
3 | | cycliswlk 26160 |
. . . . . 6
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
4 | | wlkbprop 26051 |
. . . . . 6
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
5 | | istrl2 26068 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
6 | | pm3.2 462 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
7 | 5, 6 | sylbid 229 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
8 | 7 | 3adant1 1072 |
. . . . . 6
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
9 | 3, 4, 8 | 3syl 18 |
. . . . 5
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝐹(𝑉 Trails 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
10 | 2, 9 | syl5com 31 |
. . . 4
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → (𝐹(𝑉 Cycles 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
11 | 1, 10 | mpcom 37 |
. . 3
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
12 | | iscycl 26153 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
14 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
15 | | f1eq2 6010 |
. . . . . . . . . . . . . 14
⊢
((0..^(#‘𝐹)) =
(0..^2) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ 𝐹:(0..^2)–1-1→dom 𝐸)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ 𝐹:(0..^2)–1-1→dom 𝐸)) |
17 | 14 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
18 | 16, 17 | anbi12d 743 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
19 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ (𝑃‘(#‘𝐹)) = (𝑃‘2)) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ ((𝑃‘0) =
(𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘2))) |
21 | 18, 20 | anbi12d 743 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 2
→ (((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ ((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘2)))) |
22 | 21 | anbi1d 737 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) ↔ (((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘2)) ∧ 𝑉 USGrph 𝐸))) |
23 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . 14
⊢ (0..^2) =
{0, 1} |
24 | 23 | raleqi 3119 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
(0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
25 | | 2wlklem 26094 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
{0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
26 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . 19
⊢ {(𝑃‘1), (𝑃‘2)} = {(𝑃‘2), (𝑃‘1)} |
27 | 26 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)}) |
28 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘2) = (𝑃‘0) → {(𝑃‘2), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)}) |
29 | 28 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘2), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)}) |
30 | 29 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃‘0) = (𝑃‘2) → ((𝐸‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})) |
31 | 27, 30 | syl5bb 271 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘0) = (𝑃‘2) → ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})) |
32 | 31 | anbi2d 736 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘0) = (𝑃‘2) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}))) |
33 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}) → (𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1))) |
34 | | usgraf1 25889 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸) |
35 | | f1f 6014 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:(0..^2)–1-1→dom 𝐸 → 𝐹:(0..^2)⟶dom 𝐸) |
36 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℕ |
37 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ∈
(0..^2) ↔ 2 ∈ ℕ) |
38 | 36, 37 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
(0..^2) |
39 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹:(0..^2)⟶dom 𝐸 ∧ 0 ∈ (0..^2)) →
(𝐹‘0) ∈ dom
𝐸) |
40 | 38, 39 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:(0..^2)⟶dom 𝐸 → (𝐹‘0) ∈ dom 𝐸) |
41 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℕ0 |
42 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 <
2 |
43 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
(0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1
< 2)) |
44 | 41, 36, 42, 43 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
(0..^2) |
45 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹:(0..^2)⟶dom 𝐸 ∧ 1 ∈ (0..^2)) →
(𝐹‘1) ∈ dom
𝐸) |
46 | 44, 45 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:(0..^2)⟶dom 𝐸 → (𝐹‘1) ∈ dom 𝐸) |
47 | 40, 46 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:(0..^2)⟶dom 𝐸 → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸)) |
48 | 35, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸)) |
49 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸)) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) ↔ (𝐹‘0) = (𝐹‘1))) |
50 | 48, 49 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐹:(0..^2)–1-1→dom 𝐸) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) ↔ (𝐹‘0) = (𝐹‘1))) |
51 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹:(0..^2)–1-1→dom 𝐸 ∧ (0 ∈ (0..^2) ∧ 1 ∈
(0..^2))) → ((𝐹‘0) = (𝐹‘1) ↔ 0 = 1)) |
52 | 38, 44, 51 | mpanr12 717 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐹‘0) = (𝐹‘1) ↔ 0 = 1)) |
53 | | ax-1ne0 9884 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ≠
0 |
54 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ≠ 0
↔ 0 ≠ 1) |
55 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ≠ 1
↔ ¬ 0 = 1) |
56 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬ 0
= 1 → (0 = 1 → (#‘𝐹) ≠ 2)) |
57 | 55, 56 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ≠ 1
→ (0 = 1 → (#‘𝐹) ≠ 2)) |
58 | 54, 57 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ≠ 0
→ (0 = 1 → (#‘𝐹) ≠ 2)) |
59 | 53, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 = 1
→ (#‘𝐹) ≠
2) |
60 | 52, 59 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐹‘0) = (𝐹‘1) → (#‘𝐹) ≠ 2)) |
61 | 60 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐹:(0..^2)–1-1→dom 𝐸) → ((𝐹‘0) = (𝐹‘1) → (#‘𝐹) ≠ 2)) |
62 | 50, 61 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐹:(0..^2)–1-1→dom 𝐸) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (#‘𝐹) ≠ 2)) |
63 | 62 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (#‘𝐹) ≠ 2))) |
64 | 34, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 USGrph 𝐸 → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (#‘𝐹) ≠ 2))) |
65 | 64 | com13 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (𝐹:(0..^2)–1-1→dom 𝐸 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
66 | 33, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}) → (𝐹:(0..^2)–1-1→dom 𝐸 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
67 | 32, 66 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃‘0) = (𝑃‘2) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹:(0..^2)–1-1→dom 𝐸 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))) |
68 | 67 | com3l 87 |
. . . . . . . . . . . . . 14
⊢ (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))) |
69 | 25, 68 | sylbi 206 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
{0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))) |
70 | 24, 69 | sylbi 206 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))) |
71 | 70 | impcom 445 |
. . . . . . . . . . 11
⊢ ((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
72 | 71 | imp31 447 |
. . . . . . . . . 10
⊢ ((((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘2)) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2) |
73 | 22, 72 | syl6bi 242 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2)) |
74 | | ax-1 6 |
. . . . . . . . 9
⊢
((#‘𝐹) ≠ 2
→ ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2)) |
75 | 73, 74 | pm2.61ine 2865 |
. . . . . . . 8
⊢ ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2) |
76 | 75 | exp31 628 |
. . . . . . 7
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
77 | 76 | 3adant2 1073 |
. . . . . 6
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
78 | 77 | adantld 482 |
. . . . 5
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
79 | 78 | adantl 481 |
. . . 4
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
80 | 13, 79 | sylbid 229 |
. . 3
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))) |
81 | 11, 80 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)) |
82 | 81 | impcom 445 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 2) |