Step | Hyp | Ref
| Expression |
1 | | trlsegvdeg.iy |
. . . . . . . 8
β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
2 | 1 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) |
3 | | trlsegvdeg.vy |
. . . . . . . 8
β’ (π β (Vtxβπ) = π) |
4 | 3 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (Vtxβπ) = π) |
5 | | fvexd 6858 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (πΉβπ) β V) |
6 | | trlsegvdeg.u |
. . . . . . . 8
β’ (π β π β π) |
7 | 6 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β π) |
8 | | fvexd 6858 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (πΌβ(πΉβπ)) β V) |
9 | | eupth2lem3.e |
. . . . . . . . 9
β’ (π β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
10 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β (πβπ) β§ π β (πβ(π + 1))) β π β (πβπ)) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β (πβπ)) |
12 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β (πβπ) β§ π β (πβ(π + 1))) β π β (πβ(π + 1))) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β (πβ(π + 1))) |
14 | 11, 13 | nelprd 4618 |
. . . . . . . . . . . 12
β’ (((πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β Β¬ π β {(πβπ), (πβ(π + 1))}) |
15 | | df-nel 3051 |
. . . . . . . . . . . 12
β’ (π β {(πβπ), (πβ(π + 1))} β Β¬ π β {(πβπ), (πβ(π + 1))}) |
16 | 14, 15 | sylibr 233 |
. . . . . . . . . . 11
β’ (((πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β {(πβπ), (πβ(π + 1))}) |
17 | | neleq2 3056 |
. . . . . . . . . . 11
β’ ((πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β (π β (πΌβ(πΉβπ)) β π β {(πβπ), (πβ(π + 1))})) |
18 | 16, 17 | syl5ibr 246 |
. . . . . . . . . 10
β’ ((πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β (((πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β (πΌβ(πΉβπ)))) |
19 | 18 | expd 417 |
. . . . . . . . 9
β’ ((πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πβπ) β (πβ(π + 1)) β ((π β (πβπ) β§ π β (πβ(π + 1))) β π β (πΌβ(πΉβπ))))) |
20 | 9, 19 | syl 17 |
. . . . . . . 8
β’ (π β ((πβπ) β (πβ(π + 1)) β ((π β (πβπ) β§ π β (πβ(π + 1))) β π β (πΌβ(πΉβπ))))) |
21 | 20 | 3imp 1112 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β (πΌβ(πΉβπ))) |
22 | 2, 4, 5, 7, 8, 21 | 1hevtxdg0 28456 |
. . . . . 6
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β ((VtxDegβπ)βπ) = 0) |
23 | 22 | oveq2d 7374 |
. . . . 5
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) = (((VtxDegβπ)βπ) + 0)) |
24 | | trlsegvdeg.v |
. . . . . . . . 9
β’ π = (VtxβπΊ) |
25 | | trlsegvdeg.i |
. . . . . . . . 9
β’ πΌ = (iEdgβπΊ) |
26 | | trlsegvdeg.f |
. . . . . . . . 9
β’ (π β Fun πΌ) |
27 | | trlsegvdeg.n |
. . . . . . . . 9
β’ (π β π β (0..^(β―βπΉ))) |
28 | | trlsegvdeg.w |
. . . . . . . . 9
β’ (π β πΉ(TrailsβπΊ)π) |
29 | | trlsegvdeg.vx |
. . . . . . . . 9
β’ (π β (Vtxβπ) = π) |
30 | | trlsegvdeg.vz |
. . . . . . . . 9
β’ (π β (Vtxβπ) = π) |
31 | | trlsegvdeg.ix |
. . . . . . . . 9
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) |
32 | | trlsegvdeg.iz |
. . . . . . . . 9
β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) |
33 | 24, 25, 26, 27, 6, 28, 29, 3, 30, 31, 1, 32 | eupth2lem3lem1 29175 |
. . . . . . . 8
β’ (π β ((VtxDegβπ)βπ) β
β0) |
34 | 33 | nn0cnd 12476 |
. . . . . . 7
β’ (π β ((VtxDegβπ)βπ) β β) |
35 | 34 | addid1d 11356 |
. . . . . 6
β’ (π β (((VtxDegβπ)βπ) + 0) = ((VtxDegβπ)βπ)) |
36 | 35 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (((VtxDegβπ)βπ) + 0) = ((VtxDegβπ)βπ)) |
37 | 23, 36 | eqtrd 2777 |
. . . 4
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) = ((VtxDegβπ)βπ)) |
38 | 37 | breq2d 5118 |
. . 3
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β 2 β₯ ((VtxDegβπ)βπ))) |
39 | 38 | notbid 318 |
. 2
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
40 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π β ((VtxDegβπ)βπ₯) = ((VtxDegβπ)βπ)) |
41 | 40 | breq2d 5118 |
. . . . . . 7
β’ (π₯ = π β (2 β₯ ((VtxDegβπ)βπ₯) β 2 β₯ ((VtxDegβπ)βπ))) |
42 | 41 | notbid 318 |
. . . . . 6
β’ (π₯ = π β (Β¬ 2 β₯
((VtxDegβπ)βπ₯) β Β¬ 2 β₯ ((VtxDegβπ)βπ))) |
43 | 42 | elrab3 3647 |
. . . . 5
β’ (π β π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
44 | 6, 43 | syl 17 |
. . . 4
β’ (π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β Β¬ 2 β₯
((VtxDegβπ)βπ))) |
45 | | eupth2lem3.o |
. . . . 5
β’ (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)})) |
46 | 45 | eleq2d 2824 |
. . . 4
β’ (π β (π β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπ)βπ₯)} β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
47 | 44, 46 | bitr3d 281 |
. . 3
β’ (π β (Β¬ 2 β₯
((VtxDegβπ)βπ) β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
48 | 47 | 3ad2ant1 1134 |
. 2
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (Β¬ 2 β₯
((VtxDegβπ)βπ) β π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}))) |
49 | 10 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β (πβπ)) |
50 | 12 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β π β (πβ(π + 1))) |
51 | 49, 50 | 2thd 265 |
. . . . . 6
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π β (πβπ) β π β (πβ(π + 1)))) |
52 | | neeq1 3007 |
. . . . . . 7
β’ (π = (πβ0) β (π β (πβπ) β (πβ0) β (πβπ))) |
53 | | neeq1 3007 |
. . . . . . 7
β’ (π = (πβ0) β (π β (πβ(π + 1)) β (πβ0) β (πβ(π + 1)))) |
54 | 52, 53 | bibi12d 346 |
. . . . . 6
β’ (π = (πβ0) β ((π β (πβπ) β π β (πβ(π + 1))) β ((πβ0) β (πβπ) β (πβ0) β (πβ(π + 1))))) |
55 | 51, 54 | syl5ibcom 244 |
. . . . 5
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π = (πβ0) β ((πβ0) β (πβπ) β (πβ0) β (πβ(π + 1))))) |
56 | 55 | pm5.32rd 579 |
. . . 4
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (((πβ0) β (πβπ) β§ π = (πβ0)) β ((πβ0) β (πβ(π + 1)) β§ π = (πβ0)))) |
57 | 49 | neneqd 2949 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β Β¬ π = (πβπ)) |
58 | | biorf 936 |
. . . . . . 7
β’ (Β¬
π = (πβπ) β (π = (πβ0) β (π = (πβπ) β¨ π = (πβ0)))) |
59 | 57, 58 | syl 17 |
. . . . . 6
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π = (πβ0) β (π = (πβπ) β¨ π = (πβ0)))) |
60 | | orcom 869 |
. . . . . 6
β’ ((π = (πβπ) β¨ π = (πβ0)) β (π = (πβ0) β¨ π = (πβπ))) |
61 | 59, 60 | bitrdi 287 |
. . . . 5
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π = (πβ0) β (π = (πβ0) β¨ π = (πβπ)))) |
62 | 61 | anbi2d 630 |
. . . 4
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (((πβ0) β (πβπ) β§ π = (πβ0)) β ((πβ0) β (πβπ) β§ (π = (πβ0) β¨ π = (πβπ))))) |
63 | 50 | neneqd 2949 |
. . . . . . 7
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β Β¬ π = (πβ(π + 1))) |
64 | | biorf 936 |
. . . . . . 7
β’ (Β¬
π = (πβ(π + 1)) β (π = (πβ0) β (π = (πβ(π + 1)) β¨ π = (πβ0)))) |
65 | 63, 64 | syl 17 |
. . . . . 6
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π = (πβ0) β (π = (πβ(π + 1)) β¨ π = (πβ0)))) |
66 | | orcom 869 |
. . . . . 6
β’ ((π = (πβ(π + 1)) β¨ π = (πβ0)) β (π = (πβ0) β¨ π = (πβ(π + 1)))) |
67 | 65, 66 | bitrdi 287 |
. . . . 5
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π = (πβ0) β (π = (πβ0) β¨ π = (πβ(π + 1))))) |
68 | 67 | anbi2d 630 |
. . . 4
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (((πβ0) β (πβ(π + 1)) β§ π = (πβ0)) β ((πβ0) β (πβ(π + 1)) β§ (π = (πβ0) β¨ π = (πβ(π + 1)))))) |
69 | 56, 62, 68 | 3bitr3d 309 |
. . 3
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (((πβ0) β (πβπ) β§ (π = (πβ0) β¨ π = (πβπ))) β ((πβ0) β (πβ(π + 1)) β§ (π = (πβ0) β¨ π = (πβ(π + 1)))))) |
70 | | eupth2lem1 29165 |
. . . 4
β’ (π β π β (π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β ((πβ0) β (πβπ) β§ (π = (πβ0) β¨ π = (πβπ))))) |
71 | 7, 70 | syl 17 |
. . 3
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β ((πβ0) β (πβπ) β§ (π = (πβ0) β¨ π = (πβπ))))) |
72 | | eupth2lem1 29165 |
. . . 4
β’ (π β π β (π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β ((πβ0) β (πβ(π + 1)) β§ (π = (πβ0) β¨ π = (πβ(π + 1)))))) |
73 | 7, 72 | syl 17 |
. . 3
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}) β ((πβ0) β (πβ(π + 1)) β§ (π = (πβ0) β¨ π = (πβ(π + 1)))))) |
74 | 69, 71, 73 | 3bitr4d 311 |
. 2
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (π β if((πβ0) = (πβπ), β
, {(πβ0), (πβπ)}) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |
75 | 39, 48, 74 | 3bitrd 305 |
1
β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (Β¬ 2 β₯
(((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β
, {(πβ0), (πβ(π + 1))}))) |