Step | Hyp | Ref
| Expression |
1 | | cyclprop 40999 |
. . 3
⊢ (𝐹(CycleS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
2 | | pthis1wlk 40933 |
. . . . 5
⊢ (𝐹(PathS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
3 | | upgr4cycl4dv4e.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
4 | 3 | upgr1wlkvtxedg 40853 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) |
5 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 4
→ (𝑃‘(#‘𝐹)) = (𝑃‘4)) |
6 | 5 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 4
→ ((𝑃‘0) =
(𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4))) |
7 | 6 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 4
→ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)))) |
8 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 4
→ (0..^(#‘𝐹)) =
(0..^4)) |
9 | | fzo0to42pr 12422 |
. . . . . . . . . . . . . . . 16
⊢ (0..^4) =
({0, 1} ∪ {2, 3}) |
10 | 8, 9 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 4
→ (0..^(#‘𝐹)) =
({0, 1} ∪ {2, 3})) |
11 | 10 | raleqdv 3121 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 4
→ (∀𝑘 ∈
(0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)) |
12 | | ralunb 3756 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)) |
13 | | c0ex 9913 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
14 | | 1ex 9914 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
15 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
16 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
17 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 + 1) =
1 |
18 | 16, 17 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
20 | 15, 19 | preq12d 4220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
21 | 20 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
23 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
24 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 + 1) =
2 |
25 | 23, 24 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
27 | 22, 26 | preq12d 4220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
28 | 27 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
29 | 13, 14, 21, 28 | ralpr 4185 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
{0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
30 | | 2ex 10969 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
V |
31 | | 3ex 10973 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
V |
32 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
33 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
34 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 + 1) =
3 |
35 | 33, 34 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
36 | 35 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
37 | 32, 36 | preq12d 4220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) |
38 | 37 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
39 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 3 → (𝑃‘𝑘) = (𝑃‘3)) |
40 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 3 → (𝑘 + 1) = (3 + 1)) |
41 | | 3p1e4 11030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (3 + 1) =
4 |
42 | 40, 41 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 3 → (𝑘 + 1) = 4) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4)) |
44 | 39, 43 | preq12d 4220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 3 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)}) |
45 | 44 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 3 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) |
46 | 30, 31, 38, 45 | ralpr 4185 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
{2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) |
47 | 29, 46 | anbi12i 729 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑘 ∈
{0, 1} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) |
48 | 12, 47 | bitri 263 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
({0, 1} ∪ {2, 3}){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) |
49 | 11, 48 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 4
→ (∀𝑘 ∈
(0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))) |
50 | 7, 49 | anbi12d 743 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 4
→ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))) |
51 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)}) |
52 | 51 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) |
53 | 52 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) |
54 | 53 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) |
55 | 54 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))) |
56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))) |
57 | | 4nn0 11188 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℕ0 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) → 4 ∈
ℕ0) |
59 | | upgr4cycl4dv4e.v |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑉 = (Vtx‘𝐺) |
60 | 59 | 1wlkp 40821 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
61 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐹) = 4
→ (0...(#‘𝐹)) =
(0...4)) |
62 | 61 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 4
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...4)⟶𝑉)) |
63 | 62 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉)) |
64 | 2, 60, 63 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹(PathS‘𝐺)𝑃 → ((#‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉)) |
65 | 64 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉) |
66 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℕ0 → 4 ∈ ℕ0) |
67 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℕ0 |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℕ0 → 0 ∈ ℕ0) |
69 | | 4pos 10993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 <
4 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℕ0 → 0 < 4) |
71 | 66, 68, 70 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4 ∈
ℕ0 → (4 ∈ ℕ0 ∧ 0 ∈
ℕ0 ∧ 0 < 4)) |
72 | | fvffz0 12326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((4
∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4)
∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉) |
73 | 71, 72 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((4
∈ ℕ0 ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉) |
74 | 73 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉) |
75 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℕ0 |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℕ0 → 1 ∈ ℕ0) |
77 | | 1lt4 11076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 <
4 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℕ0 → 1 < 4) |
79 | 66, 76, 78 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4 ∈
ℕ0 → (4 ∈ ℕ0 ∧ 1 ∈
ℕ0 ∧ 1 < 4)) |
80 | | fvffz0 12326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((4
∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4)
∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉) |
81 | 79, 80 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((4
∈ ℕ0 ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉) |
82 | 81 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉) |
83 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ0 |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 ∈
ℕ0 → 2 ∈ ℕ0) |
85 | | 2lt4 11075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 <
4 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 ∈
ℕ0 → 2 < 4) |
87 | 66, 84, 86 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℕ0 → (4 ∈ ℕ0 ∧ 2 ∈
ℕ0 ∧ 2 < 4)) |
88 | | fvffz0 12326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((4
∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4)
∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉) |
89 | 87, 88 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((4
∈ ℕ0 ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉) |
90 | 89 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉) |
91 | | 3nn0 11187 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 3 ∈
ℕ0 |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 ∈
ℕ0 → 3 ∈ ℕ0) |
93 | | 3lt4 11074 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 3 <
4 |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 ∈
ℕ0 → 3 < 4) |
95 | 66, 92, 94 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (4 ∈
ℕ0 → (4 ∈ ℕ0 ∧ 3 ∈
ℕ0 ∧ 3 < 4)) |
96 | | fvffz0 12326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((4
∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4)
∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉) |
97 | 95, 96 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((4
∈ ℕ0 ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉) |
98 | 97 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉) |
99 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) |
100 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) → 𝐹(PathS‘𝐺)𝑃) |
101 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) = 4
→ (1 < (#‘𝐹)
↔ 1 < 4)) |
102 | 77, 101 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) = 4
→ 1 < (#‘𝐹)) |
103 | 102 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) → 1 < (#‘𝐹)) |
104 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) → (#‘𝐹) = 4) |
105 | 8 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) → (0..^(#‘𝐹)) = (0..^4)) |
106 | | 4nn 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 4 ∈
ℕ |
107 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (0 ∈
(0..^4) ↔ 4 ∈ ℕ) |
108 | 106, 107 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 0 ∈
(0..^4) |
109 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((0..^(#‘𝐹)) =
(0..^4) → (0 ∈ (0..^(#‘𝐹)) ↔ 0 ∈
(0..^4))) |
110 | 108, 109 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0..^(#‘𝐹)) =
(0..^4) → 0 ∈ (0..^(#‘𝐹))) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐹) = 4
∧ (0..^(#‘𝐹)) =
(0..^4)) → 0 ∈ (0..^(#‘𝐹))) |
112 | | pthdadjvtx 40936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1))) |
113 | 111, 112 | syl3an3 1353 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1))) |
114 | | 1e0p1 11428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 = (0 +
1) |
115 | 114 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃‘1) = (𝑃‘(0 + 1)) |
116 | 115 | neeq2i 2847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 +
1))) |
117 | 113, 116 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1)) |
118 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → 𝐹(PathS‘𝐺)𝑃) |
119 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (2 ∈
(0..^4) ↔ (2 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 2
< 4)) |
120 | 83, 106, 85, 119 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 2 ∈
(0..^4) |
121 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 2 ≠
0 |
122 | | fzo1fzo0n0 12386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (2 ∈
(1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0)) |
123 | 120, 121,
122 | mpbir2an 957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 2 ∈
(1..^4) |
124 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐹) = 4
→ (1..^(#‘𝐹)) =
(1..^4)) |
125 | 123, 124 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 4
→ 2 ∈ (1..^(#‘𝐹))) |
126 | | 0elfz 12305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (4 ∈
ℕ0 → 0 ∈ (0...4)) |
127 | 57, 126 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 0 ∈
(0...4) |
128 | 127, 61 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 4
→ 0 ∈ (0...(#‘𝐹))) |
129 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 4
→ 2 ≠ 0) |
130 | 125, 128,
129 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 4
→ (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠
0)) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝐹) = 4
∧ (0..^(#‘𝐹)) =
(0..^4)) → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠
0)) |
132 | 131 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (2 ∈
(1..^(#‘𝐹)) ∧ 0
∈ (0...(#‘𝐹))
∧ 2 ≠ 0)) |
133 | | pthdivtx 40935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈
(0...(#‘𝐹)) ∧ 2
≠ 0)) → (𝑃‘2)
≠ (𝑃‘0)) |
134 | 118, 132,
133 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0)) |
135 | 134 | necomd 2837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2)) |
136 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (3 ∈
(0..^4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 3
< 4)) |
137 | 91, 106, 93, 136 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 3 ∈
(0..^4) |
138 | | 3ne0 10992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 3 ≠
0 |
139 | | fzo1fzo0n0 12386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (3 ∈
(1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0)) |
140 | 137, 138,
139 | mpbir2an 957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 3 ∈
(1..^4) |
141 | 140, 124 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 4
→ 3 ∈ (1..^(#‘𝐹))) |
142 | 138 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) = 4
→ 3 ≠ 0) |
143 | 141, 128,
142 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 4
→ (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠
0)) |
144 | 143 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝐹) = 4
∧ (0..^(#‘𝐹)) =
(0..^4)) → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠
0)) |
145 | 144 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (3 ∈
(1..^(#‘𝐹)) ∧ 0
∈ (0...(#‘𝐹))
∧ 3 ≠ 0)) |
146 | | pthdivtx 40935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈
(0...(#‘𝐹)) ∧ 3
≠ 0)) → (𝑃‘3)
≠ (𝑃‘0)) |
147 | 118, 145,
146 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0)) |
148 | 147 | necomd 2837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3)) |
149 | 117, 135,
148 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))) |
150 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (1 ∈
(0..^4) ↔ (1 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 1
< 4)) |
151 | 75, 106, 77, 150 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
(0..^4) |
152 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((0..^(#‘𝐹)) =
(0..^4) → (1 ∈ (0..^(#‘𝐹)) ↔ 1 ∈
(0..^4))) |
153 | 151, 152 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0..^(#‘𝐹)) =
(0..^4) → 1 ∈ (0..^(#‘𝐹))) |
154 | 153 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐹) = 4
∧ (0..^(#‘𝐹)) =
(0..^4)) → 1 ∈ (0..^(#‘𝐹))) |
155 | | pthdadjvtx 40936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1))) |
156 | 154, 155 | syl3an3 1353 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1))) |
157 | | df-2 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 = (1 +
1) |
158 | 157 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃‘2) = (𝑃‘(1 + 1)) |
159 | 158 | neeq2i 2847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 +
1))) |
160 | 156, 159 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2)) |
161 | | ax-1ne0 9884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 ≠
0 |
162 | | fzo1fzo0n0 12386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (1 ∈
(1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0)) |
163 | 151, 161,
162 | mpbir2an 957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 1 ∈
(1..^4) |
164 | 163, 124 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 4
→ 1 ∈ (1..^(#‘𝐹))) |
165 | | 3re 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 3 ∈
ℝ |
166 | | 4re 10974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 4 ∈
ℝ |
167 | 165, 166,
93 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 3 ≤
4 |
168 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (3 ∈
(0...4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0
∧ 3 ≤ 4)) |
169 | 91, 57, 167, 168 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 3 ∈
(0...4) |
170 | 169, 61 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 4
→ 3 ∈ (0...(#‘𝐹))) |
171 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 ∈
ℝ |
172 | | 1lt3 11073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 <
3 |
173 | 171, 172 | ltneii 10029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 1 ≠
3 |
174 | 173 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 4
→ 1 ≠ 3) |
175 | 164, 170,
174 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) = 4
→ (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠
3)) |
176 | 175 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐹) = 4
∧ (0..^(#‘𝐹)) =
(0..^4)) → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠
3)) |
177 | 176 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (1 ∈
(1..^(#‘𝐹)) ∧ 3
∈ (0...(#‘𝐹))
∧ 1 ≠ 3)) |
178 | | pthdivtx 40935 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈
(0...(#‘𝐹)) ∧ 1
≠ 3)) → (𝑃‘1)
≠ (𝑃‘3)) |
179 | 118, 177,
178 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3)) |
180 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((0..^(#‘𝐹)) =
(0..^4) → (2 ∈ (0..^(#‘𝐹)) ↔ 2 ∈
(0..^4))) |
181 | 120, 180 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0..^(#‘𝐹)) =
(0..^4) → 2 ∈ (0..^(#‘𝐹))) |
182 | 181 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐹) = 4
∧ (0..^(#‘𝐹)) =
(0..^4)) → 2 ∈ (0..^(#‘𝐹))) |
183 | | pthdadjvtx 40936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 2 ∈ (0..^(#‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1))) |
184 | 182, 183 | syl3an3 1353 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1))) |
185 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 3 = (2 +
1) |
186 | 185 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃‘3) = (𝑃‘(2 + 1)) |
187 | 186 | neeq2i 2847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 +
1))) |
188 | 184, 187 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3)) |
189 | 160, 179,
188 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))) |
190 | 149, 189 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))) |
191 | 100, 103,
104, 105, 190 | syl112anc 1322 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))) |
192 | 191 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))) |
193 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)}) |
194 | 193 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)) |
195 | 194 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))) |
196 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑}) |
197 | 196 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸)) |
198 | 197 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))) |
199 | 195, 198 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))) |
200 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2))) |
201 | 200 | 3anbi2d 1396 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑))) |
202 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2))) |
203 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑃‘2) → (𝑐 ≠ 𝑑 ↔ (𝑃‘2) ≠ 𝑑)) |
204 | 202, 203 | 3anbi13d 1393 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))) |
205 | 201, 204 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))) |
206 | 199, 205 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = (𝑃‘2) → (((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))) |
207 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)}) |
208 | 207 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) |
209 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)}) |
210 | 209 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) |
211 | 208, 210 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) |
212 | 211 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))) |
213 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3))) |
214 | 213 | 3anbi3d 1397 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))) |
215 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3))) |
216 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3))) |
217 | 215, 216 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))) |
218 | 214, 217 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = (𝑃‘3) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))) |
219 | 212, 218 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 = (𝑃‘3) → (((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))))) |
220 | 206, 219 | rspc2ev 3295 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃‘2) ∈ 𝑉 ∧ (𝑃‘3) ∈ 𝑉 ∧ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))) → ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) |
221 | 90, 98, 99, 192, 220 | syl112anc 1322 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) |
222 | 74, 82, 221 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0 ∧
𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))) |
223 | 222 | exp31 628 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) → ((4 ∈ ℕ0
∧ 𝑃:(0...4)⟶𝑉) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))) |
224 | 58, 65, 223 | mp2and 711 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
225 | 224 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
226 | 56, 225 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢
((((#‘𝐹) = 4
∧ 𝐹(PathS‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
227 | 226 | exp31 628 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 4
→ (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))) |
228 | 227 | imp4c 615 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 4
→ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
229 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏}) |
230 | 229 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸)) |
231 | 230 | anbi1d 737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))) |
232 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)}) |
233 | 232 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸)) |
234 | 233 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))) |
235 | 231, 234 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))) |
236 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑏 ↔ (𝑃‘0) ≠ 𝑏)) |
237 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑐 ↔ (𝑃‘0) ≠ 𝑐)) |
238 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑃‘0) → (𝑎 ≠ 𝑑 ↔ (𝑃‘0) ≠ 𝑑)) |
239 | 236, 237,
238 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑃‘0) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑))) |
240 | 239 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑃‘0) → (((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) |
241 | 235, 240 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))) |
242 | 241 | 2rexbidv 3039 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑃‘0) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))) |
243 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)}) |
244 | 243 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸)) |
245 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐}) |
246 | 245 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸)) |
247 | 244, 246 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸))) |
248 | 247 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))) |
249 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1))) |
250 | 249 | 3anbi1d 1395 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑))) |
251 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑐 ↔ (𝑃‘1) ≠ 𝑐)) |
252 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑃‘1) → (𝑏 ≠ 𝑑 ↔ (𝑃‘1) ≠ 𝑑)) |
253 | 251, 252 | 3anbi12d 1392 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑃‘1) → ((𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) |
254 | 250, 253 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) |
255 | 248, 254 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))) |
256 | 255 | 2rexbidv 3039 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑃‘1) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))) ↔ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))) |
257 | 242, 256 | rspc2ev 3295 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) |
258 | 228, 257 | syl6 34 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 4
→ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))) |
259 | 50, 258 | sylbid 229 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 4
→ (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))) |
260 | 259 | expd 451 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 4
→ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
261 | 260 | com13 86 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
262 | 4, 261 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
263 | 262 | expcom 450 |
. . . . . . 7
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))) |
264 | 263 | com23 84 |
. . . . . 6
⊢ (𝐹(1Walks‘𝐺)𝑃 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))) |
265 | 264 | expd 451 |
. . . . 5
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))))) |
266 | 2, 265 | mpcom 37 |
. . . 4
⊢ (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))))) |
267 | 266 | imp 444 |
. . 3
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
268 | 1, 267 | syl 17 |
. 2
⊢ (𝐹(CycleS‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))))) |
269 | 268 | 3imp21 1269 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(CycleS‘𝐺)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) |