Step | Hyp | Ref
| Expression |
1 | | icccmp.9 |
. . . 4
β’ (π β (π΄[,]π΅) β βͺ π) |
2 | | icccmp.4 |
. . . . . . . 8
β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} |
3 | 2 | ssrab3 4044 |
. . . . . . 7
β’ π β (π΄[,]π΅) |
4 | | icccmp.5 |
. . . . . . . 8
β’ (π β π΄ β β) |
5 | | icccmp.6 |
. . . . . . . 8
β’ (π β π΅ β β) |
6 | | iccssre 13355 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
7 | 4, 5, 6 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΄[,]π΅) β β) |
8 | 3, 7 | sstrid 3959 |
. . . . . 6
β’ (π β π β β) |
9 | | icccmp.1 |
. . . . . . . . 9
β’ π½ = (topGenβran
(,)) |
10 | | icccmp.2 |
. . . . . . . . 9
β’ π = (π½ βΎt (π΄[,]π΅)) |
11 | | icccmp.3 |
. . . . . . . . 9
β’ π· = ((abs β β )
βΎ (β Γ β)) |
12 | | icccmp.7 |
. . . . . . . . 9
β’ (π β π΄ β€ π΅) |
13 | | icccmp.8 |
. . . . . . . . 9
β’ (π β π β π½) |
14 | 9, 10, 11, 2, 4, 5,
12, 13, 1 | icccmplem1 24208 |
. . . . . . . 8
β’ (π β (π΄ β π β§ βπ¦ β π π¦ β€ π΅)) |
15 | 14 | simpld 496 |
. . . . . . 7
β’ (π β π΄ β π) |
16 | 15 | ne0d 4299 |
. . . . . 6
β’ (π β π β β
) |
17 | 14 | simprd 497 |
. . . . . . 7
β’ (π β βπ¦ β π π¦ β€ π΅) |
18 | | brralrspcev 5169 |
. . . . . . 7
β’ ((π΅ β β β§
βπ¦ β π π¦ β€ π΅) β βπ£ β β βπ¦ β π π¦ β€ π£) |
19 | 5, 17, 18 | syl2anc 585 |
. . . . . 6
β’ (π β βπ£ β β βπ¦ β π π¦ β€ π£) |
20 | 8, 16, 19 | suprcld 12126 |
. . . . 5
β’ (π β sup(π, β, < ) β
β) |
21 | 8, 16, 19, 15 | suprubd 12125 |
. . . . 5
β’ (π β π΄ β€ sup(π, β, < )) |
22 | | suprleub 12129 |
. . . . . . 7
β’ (((π β β β§ π β β
β§ βπ£ β β βπ¦ β π π¦ β€ π£) β§ π΅ β β) β (sup(π, β, < ) β€ π΅ β βπ¦ β π π¦ β€ π΅)) |
23 | 8, 16, 19, 5, 22 | syl31anc 1374 |
. . . . . 6
β’ (π β (sup(π, β, < ) β€ π΅ β βπ¦ β π π¦ β€ π΅)) |
24 | 17, 23 | mpbird 257 |
. . . . 5
β’ (π β sup(π, β, < ) β€ π΅) |
25 | | elicc2 13338 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β
(sup(π, β, < )
β (π΄[,]π΅) β (sup(π, β, < ) β β β§ π΄ β€ sup(π, β, < ) β§ sup(π, β, < ) β€ π΅))) |
26 | 4, 5, 25 | syl2anc 585 |
. . . . 5
β’ (π β (sup(π, β, < ) β (π΄[,]π΅) β (sup(π, β, < ) β β β§ π΄ β€ sup(π, β, < ) β§ sup(π, β, < ) β€ π΅))) |
27 | 20, 21, 24, 26 | mpbir3and 1343 |
. . . 4
β’ (π β sup(π, β, < ) β (π΄[,]π΅)) |
28 | 1, 27 | sseldd 3949 |
. . 3
β’ (π β sup(π, β, < ) β βͺ π) |
29 | | eluni2 4873 |
. . 3
β’
(sup(π, β,
< ) β βͺ π β βπ’ β π sup(π, β, < ) β π’) |
30 | 28, 29 | sylib 217 |
. 2
β’ (π β βπ’ β π sup(π, β, < ) β π’) |
31 | 13 | sselda 3948 |
. . . . 5
β’ ((π β§ π’ β π) β π’ β π½) |
32 | 11 | rexmet 24177 |
. . . . . . 7
β’ π· β
(βMetββ) |
33 | | eqid 2733 |
. . . . . . . . . 10
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
34 | 11, 33 | tgioo 24182 |
. . . . . . . . 9
β’
(topGenβran (,)) = (MetOpenβπ·) |
35 | 9, 34 | eqtri 2761 |
. . . . . . . 8
β’ π½ = (MetOpenβπ·) |
36 | 35 | mopni2 23872 |
. . . . . . 7
β’ ((π· β
(βMetββ) β§ π’ β π½ β§ sup(π, β, < ) β π’) β βπ€ β β+ (sup(π, β, <
)(ballβπ·)π€) β π’) |
37 | 32, 36 | mp3an1 1449 |
. . . . . 6
β’ ((π’ β π½ β§ sup(π, β, < ) β π’) β βπ€ β β+ (sup(π, β, <
)(ballβπ·)π€) β π’) |
38 | 37 | ex 414 |
. . . . 5
β’ (π’ β π½ β (sup(π, β, < ) β π’ β βπ€ β β+ (sup(π, β, <
)(ballβπ·)π€) β π’)) |
39 | 31, 38 | syl 17 |
. . . 4
β’ ((π β§ π’ β π) β (sup(π, β, < ) β π’ β βπ€ β β+ (sup(π, β, <
)(ballβπ·)π€) β π’)) |
40 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β π΄ β β) |
41 | 5 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β π΅ β β) |
42 | 12 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β π΄ β€ π΅) |
43 | 13 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β π β π½) |
44 | 1 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β (π΄[,]π΅) β βͺ π) |
45 | | simplr 768 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β π’ β π) |
46 | | simprl 770 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β π€ β β+) |
47 | | simprr 772 |
. . . . . 6
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β (sup(π, β, < )(ballβπ·)π€) β π’) |
48 | | eqid 2733 |
. . . . . 6
β’ sup(π, β, < ) = sup(π, β, <
) |
49 | | eqid 2733 |
. . . . . 6
β’
if((sup(π, β,
< ) + (π€ / 2)) β€
π΅, (sup(π, β, < ) + (π€ / 2)), π΅) = if((sup(π, β, < ) + (π€ / 2)) β€ π΅, (sup(π, β, < ) + (π€ / 2)), π΅) |
50 | 9, 10, 11, 2, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49 | icccmplem2 24209 |
. . . . 5
β’ (((π β§ π’ β π) β§ (π€ β β+ β§ (sup(π, β, <
)(ballβπ·)π€) β π’)) β π΅ β π) |
51 | 50 | rexlimdvaa 3150 |
. . . 4
β’ ((π β§ π’ β π) β (βπ€ β β+ (sup(π, β, <
)(ballβπ·)π€) β π’ β π΅ β π)) |
52 | 39, 51 | syld 47 |
. . 3
β’ ((π β§ π’ β π) β (sup(π, β, < ) β π’ β π΅ β π)) |
53 | 52 | rexlimdva 3149 |
. 2
β’ (π β (βπ’ β π sup(π, β, < ) β π’ β π΅ β π)) |
54 | 30, 53 | mpd 15 |
1
β’ (π β π΅ β π) |