Step | Hyp | Ref
| Expression |
1 | | cycliswlk 26160 |
. . . . 5
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
2 | | wlkbprop 26051 |
. . . . 5
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
4 | | iscycl 26153 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
5 | | ispth 26098 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
6 | | istrl 26067 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
7 | | fzo0to3tp 12421 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0..^3) =
{0, 1, 2} |
8 | 7 | raleqi 3119 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑘 ∈
(0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1, 2} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
9 | | 0z 11265 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℤ |
10 | | 1z 11284 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
11 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
12 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) |
13 | 12 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 0 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘0))) |
14 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
15 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
16 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 + 1) =
1 |
17 | 15, 16 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
18 | 17 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
19 | 14, 18 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
20 | 13, 19 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 0 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
22 | 21 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 1 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘1))) |
23 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
24 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
25 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 + 1) =
2 |
26 | 24, 25 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
27 | 26 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
28 | 23, 27 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
29 | 22, 28 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 1 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
30 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 2 → (𝐹‘𝑘) = (𝐹‘2)) |
31 | 30 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 2 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘2))) |
32 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
33 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
34 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 + 1) =
3 |
35 | 33, 34 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
36 | 35 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
37 | 32, 36 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) |
38 | 31, 37 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 2 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})) |
39 | 20, 29, 38 | raltpg 4183 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ) →
(∀𝑘 ∈ {0, 1, 2}
(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}))) |
40 | 9, 10, 11, 39 | mp3an 1416 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑘 ∈
{0, 1, 2} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})) |
41 | 8, 40 | bitri 263 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})) |
42 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
43 | 42 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
44 | 43 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘3) → ((𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)} ↔ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)})) |
45 | 44 | 3anbi3d 1397 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) = (𝑃‘3) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}) ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)}))) |
46 | | 3pos 10991 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 <
3 |
47 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 3
→ (0 < (#‘𝐹)
↔ 0 < 3)) |
48 | 46, 47 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 3
→ 0 < (#‘𝐹)) |
49 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 0 ∈
ℕ0 |
50 | 48, 49 | jctil 558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) = 3
→ (0 ∈ ℕ0 ∧ 0 < (#‘𝐹))) |
51 | | nvnencycllem 26171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (0 ∈ ℕ0 ∧
0 < (#‘𝐹))) →
((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → {(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸)) |
52 | 50, 51 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 3) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → {(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸)) |
53 | | 1lt3 11073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 1 <
3 |
54 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 3
→ (1 < (#‘𝐹)
↔ 1 < 3)) |
55 | 53, 54 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 3
→ 1 < (#‘𝐹)) |
56 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℕ0 |
57 | 55, 56 | jctil 558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) = 3
→ (1 ∈ ℕ0 ∧ 1 < (#‘𝐹))) |
58 | | nvnencycllem 26171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (1 ∈ ℕ0 ∧
1 < (#‘𝐹))) →
((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸)) |
59 | 57, 58 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 3) → ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸)) |
60 | | 2lt3 11072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 2 <
3 |
61 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 3
→ (2 < (#‘𝐹)
↔ 2 < 3)) |
62 | 60, 61 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 3
→ 2 < (#‘𝐹)) |
63 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℕ0 |
64 | 62, 63 | jctil 558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) = 3
→ (2 ∈ ℕ0 ∧ 2 < (#‘𝐹))) |
65 | | nvnencycllem 26171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (2 ∈ ℕ0 ∧
2 < (#‘𝐹))) →
((𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)} → {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸)) |
66 | 64, 65 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 3) → ((𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)} → {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸)) |
67 | 52, 59, 66 | 3anim123d 1398 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 3) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)}) → ({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸))) |
68 | 67 | adantlrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Fun
𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹)) ∧ (#‘𝐹) = 3) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)}) → ({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸))) |
69 | 68 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((Fun
𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹)) ∧ (#‘𝐹) = 3) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)})) → ({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸)) |
70 | | 3z 11287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 3 ∈
ℤ |
71 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (3 ∈
ℤ → 3 ∈ (ℤ≥‘3)) |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 3 ∈
(ℤ≥‘3) |
73 | | 4fvwrd4 12328 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((3
∈ (ℤ≥‘3) ∧ 𝑃:(0...3)⟶𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) |
74 | 72, 73 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃:(0...3)⟶𝑉 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) |
75 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑) → (𝑃‘2) = 𝑐) |
76 | 75 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) → (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (𝑃‘2) = 𝑐)) |
77 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) ↔ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ (𝑃‘2) = 𝑐)) |
78 | 76, 77 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) → ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐)) |
79 | 78 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑑 ∈
𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) → ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐)) |
80 | 79 | reximi 2994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑐 ∈
𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) → ∃𝑐 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐)) |
81 | 80 | reximi 2994 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐)) |
82 | 81 | reximi 2994 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐)) |
83 | 74, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃:(0...3)⟶𝑉 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐)) |
84 | | preq12 4214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) → {(𝑃‘0), (𝑃‘1)} = {𝑎, 𝑏}) |
85 | 84 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → {(𝑃‘0), (𝑃‘1)} = {𝑎, 𝑏}) |
86 | 85 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → ({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ↔ {𝑎, 𝑏} ∈ ran 𝐸)) |
87 | | preq12 4214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → {(𝑃‘1), (𝑃‘2)} = {𝑏, 𝑐}) |
88 | 87 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → {(𝑃‘1), (𝑃‘2)} = {𝑏, 𝑐}) |
89 | 88 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → ({(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ↔ {𝑏, 𝑐} ∈ ran 𝐸)) |
90 | | preq12 4214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑃‘2) = 𝑐 ∧ (𝑃‘0) = 𝑎) → {(𝑃‘2), (𝑃‘0)} = {𝑐, 𝑎}) |
91 | 90 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘2) = 𝑐) → {(𝑃‘2), (𝑃‘0)} = {𝑐, 𝑎}) |
92 | 91 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → {(𝑃‘2), (𝑃‘0)} = {𝑐, 𝑎}) |
93 | 92 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → ({(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸 ↔ {𝑐, 𝑎} ∈ ran 𝐸)) |
94 | 86, 89, 93 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → (({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸) ↔ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
95 | 94 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸) → (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
96 | 95 | reximdv 2999 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸) → (∃𝑐 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
97 | 96 | reximdv 2999 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
98 | 97 | reximdv 2999 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ ran 𝐸) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏 ∧ (𝑃‘2) = 𝑐) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
99 | 69, 83, 98 | syl2im 39 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((Fun
𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹)) ∧ (#‘𝐹) = 3) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)})) → (𝑃:(0...3)⟶𝑉 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
100 | 99 | exp41 636 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Fun
𝐸 → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → ((#‘𝐹) = 3 → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)}) → (𝑃:(0...3)⟶𝑉 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))))) |
101 | 100 | com14 94 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)}) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → ((#‘𝐹) = 3 → (Fun 𝐸 → (𝑃:(0...3)⟶𝑉 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))))) |
102 | 101 | com35 96 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘0)}) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → (𝑃:(0...3)⟶𝑉 → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))))) |
103 | 45, 102 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = (𝑃‘3) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → (𝑃:(0...3)⟶𝑉 → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))))) |
104 | 103 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}) → ((𝑃‘0) = (𝑃‘3) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → (𝑃:(0...3)⟶𝑉 → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))))) |
105 | 104 | com24 93 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}) → (𝑃:(0...3)⟶𝑉 → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → ((𝑃‘0) = (𝑃‘3) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))))) |
106 | 41, 105 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
(0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃:(0...3)⟶𝑉 → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → ((𝑃‘0) = (𝑃‘3) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))))) |
107 | 106 | com13 86 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) → (𝑃:(0...3)⟶𝑉 → (∀𝑘 ∈ (0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝑃‘0) = (𝑃‘3) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))))) |
108 | 107 | 3imp 1249 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...3)⟶𝑉 ∧ ∀𝑘 ∈ (0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘3) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
109 | 108 | com14 94 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 3
→ ((𝑃‘0) =
(𝑃‘3) → (Fun
𝐸 → (((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...3)⟶𝑉 ∧ ∀𝑘 ∈ (0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
110 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 3
→ (𝑃‘(#‘𝐹)) = (𝑃‘3)) |
111 | 110 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 3
→ ((𝑃‘0) =
(𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3))) |
112 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 3
→ (0...(#‘𝐹)) =
(0...3)) |
113 | 112 | feq2d 5944 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 3
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉)) |
114 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 3
→ (0..^(#‘𝐹)) =
(0..^3)) |
115 | 114 | raleqdv 3121 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 3
→ (∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
116 | 113, 115 | 3anbi23d 1394 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 3
→ (((𝐹 ∈ Word dom
𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...3)⟶𝑉 ∧ ∀𝑘 ∈ (0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
117 | 116 | imbi1d 330 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 3
→ ((((𝐹 ∈ Word
dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) ↔ (((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...3)⟶𝑉 ∧ ∀𝑘 ∈ (0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
118 | 117 | imbi2d 329 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 3
→ ((Fun 𝐸 →
(((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) ↔ (Fun 𝐸 → (((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...3)⟶𝑉 ∧ ∀𝑘 ∈ (0..^3)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
119 | 109, 111,
118 | 3imtr4d 282 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 3
→ ((𝑃‘0) =
(𝑃‘(#‘𝐹)) → (Fun 𝐸 → (((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
120 | 119 | com14 94 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
121 | 120 | 2a1d 26 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))))) |
122 | 6, 121 | syl6bi 242 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))))))) |
123 | 122 | 3impd 1273 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))))) |
124 | 5, 123 | sylbid 229 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))))) |
125 | 124 | impd 446 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
126 | 4, 125 | sylbid 229 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
127 | 126 | 3adant1 1072 |
. . . 4
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
128 | 3, 127 | mpcom 37 |
. . 3
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (Fun 𝐸 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
129 | 128 | com12 32 |
. 2
⊢ (Fun
𝐸 → (𝐹(𝑉 Cycles 𝐸)𝑃 → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
130 | 129 | 3imp 1249 |
1
⊢ ((Fun
𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) |