Step | Hyp | Ref
| Expression |
1 | | cyclprop 40999 |
. . 3
⊢ (𝐹(CycleS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
2 | | pthis1wlk 40933 |
. . . . 5
⊢ (𝐹(PathS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
3 | | upgr3v3e3cycl.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
4 | 3 | upgr1wlkvtxedg 40853 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) |
5 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 3
→ (𝑃‘(#‘𝐹)) = (𝑃‘3)) |
6 | 5 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 3
→ ((𝑃‘0) =
(𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3))) |
7 | 6 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 3
→ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)))) |
8 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 3
→ (0..^(#‘𝐹)) =
(0..^3)) |
9 | | fzo0to3tp 12421 |
. . . . . . . . . . . . . . . 16
⊢ (0..^3) =
{0, 1, 2} |
10 | 8, 9 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 3
→ (0..^(#‘𝐹)) =
{0, 1, 2}) |
11 | 10 | raleqdv 3121 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 3
→ (∀𝑘 ∈
(0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)) |
12 | | c0ex 9913 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
13 | | 1ex 9914 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
14 | | 2ex 10969 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
V |
15 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
16 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
17 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 + 1) =
1 |
18 | 16, 17 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
20 | 15, 19 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
21 | 20 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
23 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
24 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 + 1) =
2 |
25 | 23, 24 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
27 | 22, 26 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
28 | 27 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
29 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
30 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
31 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 + 1) =
3 |
32 | 30, 31 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
33 | 32 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
34 | 29, 33 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) |
35 | 34 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
36 | 12, 13, 14, 21, 28, 35 | raltp 4187 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
{0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
37 | 11, 36 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 3
→ (∀𝑘 ∈
(0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) |
38 | 7, 37 | anbi12d 743 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 3
→ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))) |
39 | | upgr3v3e3cycl.v |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑉 = (Vtx‘𝐺) |
40 | 39 | 1wlkp 40821 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
41 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 3
→ (0...(#‘𝐹)) =
(0...3)) |
42 | 41 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 3
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉)) |
43 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃:(0...3)⟶𝑉 → 𝑃:(0...3)⟶𝑉) |
44 | | 3nn0 11187 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 3 ∈
ℕ0 |
45 | | 0elfz 12305 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (3 ∈
ℕ0 → 0 ∈ (0...3)) |
46 | 44, 45 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃:(0...3)⟶𝑉 → 0 ∈
(0...3)) |
47 | 43, 46 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉) |
48 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℕ0 |
49 | | 1lt3 11073 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 <
3 |
50 | | fvffz0 12326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((3
∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3)
∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉) |
51 | 50 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3)
→ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)) |
52 | 44, 48, 49, 51 | mp3an 1416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉) |
53 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℕ0 |
54 | | 2lt3 11072 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 <
3 |
55 | | fvffz0 12326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((3
∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3)
∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉) |
56 | 55 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3)
→ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)) |
57 | 44, 53, 54, 56 | mp3an 1416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉) |
58 | 47, 52, 57 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
59 | 42, 58 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 3
→ (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
60 | 59 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
61 | 2, 40, 60 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹(PathS‘𝐺)𝑃 → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
64 | 63 | impcom 445 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 3
∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
65 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
66 | 65 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
68 | 67 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
69 | 68 | 3anbi3d 1397 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))) |
70 | 69 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 3
∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
72 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 𝐹(PathS‘𝐺)𝑃) |
73 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 3
→ (1 < (#‘𝐹)
↔ 1 < 3)) |
74 | 49, 73 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 3
→ 1 < (#‘𝐹)) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 1 < (#‘𝐹)) |
76 | | 3nn 11063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℕ |
77 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
(0..^3) ↔ 3 ∈ ℕ) |
78 | 76, 77 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
(0..^3) |
79 | 78, 8 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 3
→ 0 ∈ (0..^(#‘𝐹))) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 0 ∈ (0..^(#‘𝐹))) |
81 | | pthdadjvtx 40936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1))) |
82 | | 1e0p1 11428 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 = (0 +
1) |
83 | 82 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃‘1) = (𝑃‘(0 + 1)) |
84 | 83 | neeq2i 2847 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 +
1))) |
85 | 81, 84 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1)) |
86 | 72, 75, 80, 85 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1)) |
87 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
(0..^3) ↔ (1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1
< 3)) |
88 | 48, 76, 49, 87 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
(0..^3) |
89 | 88, 8 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 3
→ 1 ∈ (0..^(#‘𝐹))) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 1 ∈ (0..^(#‘𝐹))) |
91 | | pthdadjvtx 40936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1))) |
92 | | df-2 10956 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 = (1 +
1) |
93 | 92 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃‘2) = (𝑃‘(1 + 1)) |
94 | 93 | neeq2i 2847 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 +
1))) |
95 | 91, 94 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2)) |
96 | 72, 75, 90, 95 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2)) |
97 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 ∈
(0..^3) ↔ (2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2
< 3)) |
98 | 53, 76, 54, 97 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
(0..^3) |
99 | 98, 8 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 3
→ 2 ∈ (0..^(#‘𝐹))) |
100 | 99 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 2 ∈ (0..^(#‘𝐹))) |
101 | | pthdadjvtx 40936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 2 ∈ (0..^(#‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1))) |
102 | 72, 75, 100, 101 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1))) |
103 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3))) |
104 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 = (2 +
1) |
105 | 104 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃‘3) = (𝑃‘(2 + 1)) |
106 | 105 | neeq2i 2847 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 +
1))) |
107 | 103, 106 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))) |
110 | 102, 109 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0)) |
111 | 86, 96, 110 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))) |
112 | 111 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((#‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
113 | 112 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((#‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
114 | 113 | impcom 445 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 3
∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))) |
115 | | preq1 4212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏}) |
116 | 115 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸)) |
117 | | preq2 4213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)}) |
118 | 117 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸)) |
119 | 116, 118 | 3anbi13d 1393 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸))) |
120 | | neeq1 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏)) |
121 | | neeq2 2845 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (𝑐 ≠ 𝑎 ↔ 𝑐 ≠ (𝑃‘0))) |
122 | 120, 121 | 3anbi13d 1393 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))) |
123 | 119, 122 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))) |
124 | | preq2 4213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)}) |
125 | 124 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
126 | | preq1 4212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐}) |
127 | 126 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸)) |
128 | 125, 127 | 3anbi12d 1392 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸))) |
129 | | neeq2 2845 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1))) |
130 | | neeq1 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐)) |
131 | 129, 130 | 3anbi12d 1392 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))) |
132 | 128, 131 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))) |
133 | | preq2 4213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)}) |
134 | 133 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
135 | | preq1 4212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)}) |
136 | 135 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
137 | 134, 136 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))) |
138 | | neeq2 2845 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2))) |
139 | | neeq1 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0))) |
140 | 138, 139 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
141 | 137, 140 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))) |
142 | 123, 132,
141 | rspc3ev 3297 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |
143 | 64, 71, 114, 142 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢
(((#‘𝐹) = 3
∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |
144 | 143 | ex 449 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 3
→ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))) |
145 | 38, 144 | sylbid 229 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 3
→ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))) |
146 | 145 | expd 451 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 3
→ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
147 | 146 | com13 86 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
148 | 4, 147 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
149 | 148 | expcom 450 |
. . . . . . 7
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
150 | 149 | com23 84 |
. . . . . 6
⊢ (𝐹(1Walks‘𝐺)𝑃 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
151 | 150 | expd 451 |
. . . . 5
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))) |
152 | 2, 151 | mpcom 37 |
. . . 4
⊢ (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
153 | 152 | imp 444 |
. . 3
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
154 | 1, 153 | syl 17 |
. 2
⊢ (𝐹(CycleS‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
155 | 154 | 3imp21 1269 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(CycleS‘𝐺)𝑃 ∧ (#‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |