Step | Hyp | Ref
| Expression |
1 | | cyclprop 26924 |
. . 3
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) |
2 | | pthiswlk 26858 |
. . . . 5
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
3 | | upgr3v3e3cycl.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
4 | 3 | upgrwlkvtxedg 26776 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) |
5 | | fveq2 6332 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹) =
3 → (𝑃‘(♯‘𝐹)) = (𝑃‘3)) |
6 | 5 | eqeq2d 2781 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹) =
3 → ((𝑃‘0) =
(𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3))) |
7 | 6 | anbi2d 614 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) =
3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)))) |
8 | | oveq2 6801 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝐹) =
3 → (0..^(♯‘𝐹)) = (0..^3)) |
9 | | fzo0to3tp 12762 |
. . . . . . . . . . . . . . . 16
⊢ (0..^3) =
{0, 1, 2} |
10 | 8, 9 | syl6eq 2821 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹) =
3 → (0..^(♯‘𝐹)) = {0, 1, 2}) |
11 | 10 | raleqdv 3293 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹) =
3 → (∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)) |
12 | | c0ex 10236 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
13 | | 1ex 10237 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
14 | | 2ex 11294 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
V |
15 | | fveq2 6332 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
16 | | oveq1 6800 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
17 | | 0p1e1 11334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 + 1) =
1 |
18 | 16, 17 | syl6eq 2821 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
19 | 18 | fveq2d 6336 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
20 | 15, 19 | preq12d 4412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
21 | 20 | eleq1d 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
22 | | fveq2 6332 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
23 | | oveq1 6800 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
24 | | 1p1e2 11336 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 + 1) =
2 |
25 | 23, 24 | syl6eq 2821 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
26 | 25 | fveq2d 6336 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
27 | 22, 26 | preq12d 4412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
28 | 27 | eleq1d 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
29 | | fveq2 6332 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
30 | | oveq1 6800 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
31 | | 2p1e3 11353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 + 1) =
3 |
32 | 30, 31 | syl6eq 2821 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
33 | 32 | fveq2d 6336 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
34 | 29, 33 | preq12d 4412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) |
35 | 34 | eleq1d 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
36 | 12, 13, 14, 21, 28, 35 | raltp 4377 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
{0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
37 | 11, 36 | syl6bb 276 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) =
3 → (∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) |
38 | 7, 37 | anbi12d 616 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))) |
39 | | upgr3v3e3cycl.v |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑉 = (Vtx‘𝐺) |
40 | 39 | wlkp 26747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
41 | | oveq2 6801 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹) =
3 → (0...(♯‘𝐹)) = (0...3)) |
42 | 41 | feq2d 6171 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉)) |
43 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃:(0...3)⟶𝑉 → 𝑃:(0...3)⟶𝑉) |
44 | | 3nn0 11512 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 3 ∈
ℕ0 |
45 | | 0elfz 12644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (3 ∈
ℕ0 → 0 ∈ (0...3)) |
46 | 44, 45 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃:(0...3)⟶𝑉 → 0 ∈
(0...3)) |
47 | 43, 46 | ffvelrnd 6503 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉) |
48 | | 1nn0 11510 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℕ0 |
49 | | 1lt3 11398 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 <
3 |
50 | | fvffz0 12665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((3
∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3)
∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉) |
51 | 50 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3)
→ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)) |
52 | 44, 48, 49, 51 | mp3an 1572 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉) |
53 | | 2nn0 11511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℕ0 |
54 | | 2lt3 11397 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 <
3 |
55 | | fvffz0 12665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((3
∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3)
∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉) |
56 | 55 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3)
→ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)) |
57 | 44, 53, 54, 56 | mp3an 1572 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉) |
58 | 47, 52, 57 | 3jca 1122 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
59 | 42, 58 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . 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 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
63 | 62 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
64 | 63 | impcom 394 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
65 | | preq2 4405 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
66 | 65 | eqcoms 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
67 | 66 | adantl 467 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
68 | 67 | eleq1d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
69 | 68 | 3anbi3d 1553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))) |
70 | 69 | biimpa 462 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
71 | 70 | adantl 467 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
72 | | simpll 750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 𝐹(Paths‘𝐺)𝑃) |
73 | | breq2 4790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹) =
3 → (1 < (♯‘𝐹) ↔ 1 < 3)) |
74 | 49, 73 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → 1 < (♯‘𝐹)) |
75 | 74 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 <
(♯‘𝐹)) |
76 | | 3nn 11388 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℕ |
77 | | lbfzo0 12716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
(0..^3) ↔ 3 ∈ ℕ) |
78 | 76, 77 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
(0..^3) |
79 | 78, 8 | syl5eleqr 2857 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → 0 ∈ (0..^(♯‘𝐹))) |
80 | 79 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 0 ∈
(0..^(♯‘𝐹))) |
81 | | pthdadjvtx 26861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘0) ≠
(𝑃‘(0 +
1))) |
82 | | 1e0p1 11754 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 = (0 +
1) |
83 | 82 | fveq2i 6335 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃‘1) = (𝑃‘(0 + 1)) |
84 | 83 | neeq2i 3008 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 +
1))) |
85 | 81, 84 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘0) ≠
(𝑃‘1)) |
86 | 72, 75, 80, 85 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1)) |
87 | | elfzo0 12717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
(0..^3) ↔ (1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1
< 3)) |
88 | 48, 76, 49, 87 | mpbir3an 1426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
(0..^3) |
89 | 88, 8 | syl5eleqr 2857 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → 1 ∈ (0..^(♯‘𝐹))) |
90 | 89 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 ∈
(0..^(♯‘𝐹))) |
91 | | pthdadjvtx 26861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘1) ≠
(𝑃‘(1 +
1))) |
92 | | df-2 11281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 = (1 +
1) |
93 | 92 | fveq2i 6335 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃‘2) = (𝑃‘(1 + 1)) |
94 | 93 | neeq2i 3008 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 +
1))) |
95 | 91, 94 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘1) ≠
(𝑃‘2)) |
96 | 72, 75, 90, 95 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2)) |
97 | | elfzo0 12717 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 ∈
(0..^3) ↔ (2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2
< 3)) |
98 | 53, 76, 54, 97 | mpbir3an 1426 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
(0..^3) |
99 | 98, 8 | syl5eleqr 2857 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹) =
3 → 2 ∈ (0..^(♯‘𝐹))) |
100 | 99 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 2 ∈
(0..^(♯‘𝐹))) |
101 | | pthdadjvtx 26861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘2) ≠
(𝑃‘(2 +
1))) |
102 | 72, 75, 100, 101 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1))) |
103 | | neeq2 3006 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3))) |
104 | | df-3 11282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 = (2 +
1) |
105 | 104 | fveq2i 6335 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃‘3) = (𝑃‘(2 + 1)) |
106 | 105 | neeq2i 3008 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 +
1))) |
107 | 103, 106 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))) |
108 | 107 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))) |
109 | 108 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 +
1)))) |
110 | 102, 109 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0)) |
111 | 86, 96, 110 | 3jca 1122 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))) |
112 | 111 | ex 397 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
113 | 112 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
114 | 113 | impcom 394 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))) |
115 | | preq1 4404 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏}) |
116 | 115 | eleq1d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸)) |
117 | | preq2 4405 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)}) |
118 | 117 | eleq1d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸)) |
119 | 116, 118 | 3anbi13d 1549 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸))) |
120 | | neeq1 3005 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏)) |
121 | | neeq2 3006 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (𝑐 ≠ 𝑎 ↔ 𝑐 ≠ (𝑃‘0))) |
122 | 120, 121 | 3anbi13d 1549 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))) |
123 | 119, 122 | anbi12d 616 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))) |
124 | | preq2 4405 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)}) |
125 | 124 | eleq1d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
126 | | preq1 4404 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐}) |
127 | 126 | eleq1d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸)) |
128 | 125, 127 | 3anbi12d 1548 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸))) |
129 | | neeq2 3006 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1))) |
130 | | neeq1 3005 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐)) |
131 | 129, 130 | 3anbi12d 1548 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))) |
132 | 128, 131 | anbi12d 616 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))) |
133 | | preq2 4405 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)}) |
134 | 133 | eleq1d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
135 | | preq1 4404 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)}) |
136 | 135 | eleq1d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
137 | 134, 136 | 3anbi23d 1550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))) |
138 | | neeq2 3006 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2))) |
139 | | neeq1 3005 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0))) |
140 | 138, 139 | 3anbi23d 1550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
141 | 137, 140 | anbi12d 616 |
. . . . . . . . . . . . . . 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 3476 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |
143 | 64, 71, 114, 142 | syl12anc 1474 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |
144 | 143 | ex 397 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))) |
145 | 38, 144 | sylbid 230 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))) |
146 | 145 | expd 400 |
. . . . . . . . . 10
⊢
((♯‘𝐹) =
3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
147 | 146 | com13 88 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
148 | 4, 147 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
149 | 148 | expcom 398 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
150 | 149 | com23 86 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
151 | 150 | expd 400 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))) |
152 | 2, 151 | mpcom 38 |
. . . 4
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
153 | 152 | imp 393 |
. . 3
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
154 | 1, 153 | syl 17 |
. 2
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
155 | 154 | 3imp21 1105 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |