Step | Hyp | Ref
| Expression |
1 | | cyclprop 28157 |
. . 3
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) |
2 | | pthiswlk 28091 |
. . . . 5
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
3 | | upgr3v3e3cycl.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
4 | 3 | upgrwlkvtxedg 28009 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) |
5 | | fveq2 6771 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹) =
3 → (𝑃‘(♯‘𝐹)) = (𝑃‘3)) |
6 | 5 | eqeq2d 2751 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹) =
3 → ((𝑃‘0) =
(𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3))) |
7 | 6 | anbi2d 629 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) =
3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)))) |
8 | | oveq2 7279 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝐹) =
3 → (0..^(♯‘𝐹)) = (0..^3)) |
9 | | fzo0to3tp 13471 |
. . . . . . . . . . . . . . . 16
⊢ (0..^3) =
{0, 1, 2} |
10 | 8, 9 | eqtrdi 2796 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹) =
3 → (0..^(♯‘𝐹)) = {0, 1, 2}) |
11 | 10 | raleqdv 3347 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹) =
3 → (∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)) |
12 | | c0ex 10970 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
13 | | 1ex 10972 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
14 | | 2ex 12050 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
V |
15 | | fveq2 6771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
16 | | fv0p1e1 12096 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
17 | 15, 16 | preq12d 4683 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
18 | 17 | eleq1d 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
19 | | fveq2 6771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
20 | | oveq1 7278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
21 | | 1p1e2 12098 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 + 1) =
2 |
22 | 20, 21 | eqtrdi 2796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
23 | 22 | fveq2d 6775 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
24 | 19, 23 | preq12d 4683 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
25 | 24 | eleq1d 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
26 | | fveq2 6771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
27 | | oveq1 7278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
28 | | 2p1e3 12115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 + 1) =
3 |
29 | 27, 28 | eqtrdi 2796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
30 | 29 | fveq2d 6775 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
31 | 26, 30 | preq12d 4683 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) |
32 | 31 | eleq1d 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
33 | 12, 13, 14, 18, 25, 32 | raltp 4647 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
{0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
34 | 11, 33 | bitrdi 287 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) =
3 → (∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) |
35 | 7, 34 | anbi12d 631 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))) |
36 | | upgr3v3e3cycl.v |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑉 = (Vtx‘𝐺) |
37 | 36 | wlkp 27981 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
38 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹) =
3 → (0...(♯‘𝐹)) = (0...3)) |
39 | 38 | feq2d 6584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...3)⟶𝑉)) |
40 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃:(0...3)⟶𝑉 → 𝑃:(0...3)⟶𝑉) |
41 | | 3nn0 12251 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 3 ∈
ℕ0 |
42 | | 0elfz 13352 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (3 ∈
ℕ0 → 0 ∈ (0...3)) |
43 | 41, 42 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃:(0...3)⟶𝑉 → 0 ∈
(0...3)) |
44 | 40, 43 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉) |
45 | | 1nn0 12249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℕ0 |
46 | | 1lt3 12146 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 <
3 |
47 | | fvffz0 13373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((3
∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3)
∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉) |
48 | 47 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3)
→ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)) |
49 | 41, 45, 46, 48 | mp3an 1460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉) |
50 | | 2nn0 12250 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℕ0 |
51 | | 2lt3 12145 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 <
3 |
52 | | fvffz0 13373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((3
∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3)
∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉) |
53 | 52 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3)
→ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)) |
54 | 41, 50, 51, 53 | mp3an 1460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉) |
55 | 44, 49, 54 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
56 | 39, 55 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝐹) =
3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
58 | 2, 37, 57 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))) |
61 | 60 | impcom 408 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)) |
62 | | preq2 4676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
63 | 62 | eqcoms 2748 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
64 | 63 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)}) |
65 | 64 | eleq1d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
66 | 65 | 3anbi3d 1441 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))) |
67 | 66 | biimpa 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
69 | | simpll 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 𝐹(Paths‘𝐺)𝑃) |
70 | | breq2 5083 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹) =
3 → (1 < (♯‘𝐹) ↔ 1 < 3)) |
71 | 46, 70 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → 1 < (♯‘𝐹)) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 <
(♯‘𝐹)) |
73 | | 3nn 12052 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℕ |
74 | | lbfzo0 13425 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
(0..^3) ↔ 3 ∈ ℕ) |
75 | 73, 74 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
(0..^3) |
76 | 75, 8 | eleqtrrid 2848 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → 0 ∈ (0..^(♯‘𝐹))) |
77 | 76 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 0 ∈
(0..^(♯‘𝐹))) |
78 | | pthdadjvtx 28094 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘0) ≠
(𝑃‘(0 +
1))) |
79 | | 1e0p1 12478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 = (0 +
1) |
80 | 79 | fveq2i 6774 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃‘1) = (𝑃‘(0 + 1)) |
81 | 80 | neeq2i 3011 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 +
1))) |
82 | 78, 81 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘0) ≠
(𝑃‘1)) |
83 | 69, 72, 77, 82 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1)) |
84 | | elfzo0 13426 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
(0..^3) ↔ (1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1
< 3)) |
85 | 45, 73, 46, 84 | mpbir3an 1340 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
(0..^3) |
86 | 85, 8 | eleqtrrid 2848 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
3 → 1 ∈ (0..^(♯‘𝐹))) |
87 | 86 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 ∈
(0..^(♯‘𝐹))) |
88 | | pthdadjvtx 28094 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘1) ≠
(𝑃‘(1 +
1))) |
89 | | df-2 12036 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 = (1 +
1) |
90 | 89 | fveq2i 6774 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃‘2) = (𝑃‘(1 + 1)) |
91 | 90 | neeq2i 3011 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 +
1))) |
92 | 88, 91 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘1) ≠
(𝑃‘2)) |
93 | 69, 72, 87, 92 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2)) |
94 | | elfzo0 13426 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 ∈
(0..^3) ↔ (2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2
< 3)) |
95 | 50, 73, 51, 94 | mpbir3an 1340 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
(0..^3) |
96 | 95, 8 | eleqtrrid 2848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹) =
3 → 2 ∈ (0..^(♯‘𝐹))) |
97 | 96 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 2 ∈
(0..^(♯‘𝐹))) |
98 | | pthdadjvtx 28094 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈
(0..^(♯‘𝐹)))
→ (𝑃‘2) ≠
(𝑃‘(2 +
1))) |
99 | 69, 72, 97, 98 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1))) |
100 | | neeq2 3009 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3))) |
101 | | df-3 12037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 = (2 +
1) |
102 | 101 | fveq2i 6774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃‘3) = (𝑃‘(2 + 1)) |
103 | 102 | neeq2i 3011 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 +
1))) |
104 | 100, 103 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))) |
105 | 104 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))) |
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 +
1)))) |
107 | 99, 106 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0)) |
108 | 83, 93, 107 | 3jca 1127 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))) |
109 | 108 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
111 | 110 | impcom 408 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))) |
112 | | preq1 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏}) |
113 | 112 | eleq1d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸)) |
114 | | preq2 4676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)}) |
115 | 114 | eleq1d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸)) |
116 | 113, 115 | 3anbi13d 1437 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸))) |
117 | | neeq1 3008 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏)) |
118 | | neeq2 3009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (𝑐 ≠ 𝑎 ↔ 𝑐 ≠ (𝑃‘0))) |
119 | 117, 118 | 3anbi13d 1437 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))) |
120 | 116, 119 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))) |
121 | | preq2 4676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)}) |
122 | 121 | eleq1d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
123 | | preq1 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐}) |
124 | 123 | eleq1d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸)) |
125 | 122, 124 | 3anbi12d 1436 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸))) |
126 | | neeq2 3009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1))) |
127 | | neeq1 3008 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐)) |
128 | 126, 127 | 3anbi12d 1436 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)))) |
129 | 125, 128 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))))) |
130 | | preq2 4676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)}) |
131 | 130 | eleq1d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
132 | | preq1 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)}) |
133 | 132 | eleq1d 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)) |
134 | 131, 133 | 3anbi23d 1438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))) |
135 | | neeq2 3009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2))) |
136 | | neeq1 3008 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0))) |
137 | 135, 136 | 3anbi23d 1438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) |
138 | 134, 137 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐 ∧ 𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))) |
139 | 120, 129,
138 | rspc3ev 3575 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |
140 | 61, 68, 111, 139 | syl12anc 834 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐹)
= 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |
141 | 140 | ex 413 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))) |
142 | 35, 141 | sylbid 239 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))) |
143 | 142 | expd 416 |
. . . . . . . . . 10
⊢
((♯‘𝐹) =
3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
144 | 143 | com13 88 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
145 | 4, 144 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
146 | 145 | expcom 414 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
147 | 146 | com23 86 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
148 | 147 | expd 416 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))))) |
149 | 2, 148 | mpcom 38 |
. . . 4
⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎)))))) |
150 | 149 | imp 407 |
. . 3
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
151 | 1, 150 | syl 17 |
. 2
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))))) |
152 | 151 | 3imp21 1113 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) |