Step | Hyp | Ref
| Expression |
1 | | eliun 5002 |
. . . . 5
β’ (π¦ β βͺ π₯ β β€ (π₯(,)(π₯ + 1)) β βπ₯ β β€ π¦ β (π₯(,)(π₯ + 1))) |
2 | | elioore 13354 |
. . . . . . . . 9
β’ (π¦ β (π₯(,)(π₯ + 1)) β π¦ β β) |
3 | 2 | adantl 483 |
. . . . . . . 8
β’ ((π₯ β β€ β§ π¦ β (π₯(,)(π₯ + 1))) β π¦ β β) |
4 | | eliooord 13383 |
. . . . . . . . 9
β’ (π¦ β (π₯(,)(π₯ + 1)) β (π₯ < π¦ β§ π¦ < (π₯ + 1))) |
5 | | btwnnz 12638 |
. . . . . . . . . 10
β’ ((π₯ β β€ β§ π₯ < π¦ β§ π¦ < (π₯ + 1)) β Β¬ π¦ β β€) |
6 | 5 | 3expb 1121 |
. . . . . . . . 9
β’ ((π₯ β β€ β§ (π₯ < π¦ β§ π¦ < (π₯ + 1))) β Β¬ π¦ β β€) |
7 | 4, 6 | sylan2 594 |
. . . . . . . 8
β’ ((π₯ β β€ β§ π¦ β (π₯(,)(π₯ + 1))) β Β¬ π¦ β β€) |
8 | 3, 7 | eldifd 3960 |
. . . . . . 7
β’ ((π₯ β β€ β§ π¦ β (π₯(,)(π₯ + 1))) β π¦ β (β β
β€)) |
9 | 8 | rexlimiva 3148 |
. . . . . 6
β’
(βπ₯ β
β€ π¦ β (π₯(,)(π₯ + 1)) β π¦ β (β β
β€)) |
10 | | eldifi 4127 |
. . . . . . . 8
β’ (π¦ β (β β
β€) β π¦ β
β) |
11 | 10 | flcld 13763 |
. . . . . . 7
β’ (π¦ β (β β
β€) β (ββπ¦) β β€) |
12 | 11 | zred 12666 |
. . . . . . . . 9
β’ (π¦ β (β β
β€) β (ββπ¦) β β) |
13 | | flle 13764 |
. . . . . . . . . 10
β’ (π¦ β β β
(ββπ¦) β€
π¦) |
14 | 10, 13 | syl 17 |
. . . . . . . . 9
β’ (π¦ β (β β
β€) β (ββπ¦) β€ π¦) |
15 | | eldifn 4128 |
. . . . . . . . . . 11
β’ (π¦ β (β β
β€) β Β¬ π¦
β β€) |
16 | | nelne2 3041 |
. . . . . . . . . . 11
β’
(((ββπ¦)
β β€ β§ Β¬ π¦ β β€) β (ββπ¦) β π¦) |
17 | 11, 15, 16 | syl2anc 585 |
. . . . . . . . . 10
β’ (π¦ β (β β
β€) β (ββπ¦) β π¦) |
18 | 17 | necomd 2997 |
. . . . . . . . 9
β’ (π¦ β (β β
β€) β π¦ β
(ββπ¦)) |
19 | 12, 10, 14, 18 | leneltd 11368 |
. . . . . . . 8
β’ (π¦ β (β β
β€) β (ββπ¦) < π¦) |
20 | | flltp1 13765 |
. . . . . . . . 9
β’ (π¦ β β β π¦ < ((ββπ¦) + 1)) |
21 | 10, 20 | syl 17 |
. . . . . . . 8
β’ (π¦ β (β β
β€) β π¦ <
((ββπ¦) +
1)) |
22 | 12 | rexrd 11264 |
. . . . . . . . 9
β’ (π¦ β (β β
β€) β (ββπ¦) β
β*) |
23 | | peano2re 11387 |
. . . . . . . . . . 11
β’
((ββπ¦)
β β β ((ββπ¦) + 1) β β) |
24 | 12, 23 | syl 17 |
. . . . . . . . . 10
β’ (π¦ β (β β
β€) β ((ββπ¦) + 1) β β) |
25 | 24 | rexrd 11264 |
. . . . . . . . 9
β’ (π¦ β (β β
β€) β ((ββπ¦) + 1) β
β*) |
26 | | elioo2 13365 |
. . . . . . . . 9
β’
(((ββπ¦)
β β* β§ ((ββπ¦) + 1) β β*) β
(π¦ β
((ββπ¦)(,)((ββπ¦) + 1)) β (π¦ β β β§ (ββπ¦) < π¦ β§ π¦ < ((ββπ¦) + 1)))) |
27 | 22, 25, 26 | syl2anc 585 |
. . . . . . . 8
β’ (π¦ β (β β
β€) β (π¦ β
((ββπ¦)(,)((ββπ¦) + 1)) β (π¦ β β β§ (ββπ¦) < π¦ β§ π¦ < ((ββπ¦) + 1)))) |
28 | 10, 19, 21, 27 | mpbir3and 1343 |
. . . . . . 7
β’ (π¦ β (β β
β€) β π¦ β
((ββπ¦)(,)((ββπ¦) + 1))) |
29 | | id 22 |
. . . . . . . . . 10
β’ (π₯ = (ββπ¦) β π₯ = (ββπ¦)) |
30 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π₯ = (ββπ¦) β (π₯ + 1) = ((ββπ¦) + 1)) |
31 | 29, 30 | oveq12d 7427 |
. . . . . . . . 9
β’ (π₯ = (ββπ¦) β (π₯(,)(π₯ + 1)) = ((ββπ¦)(,)((ββπ¦) + 1))) |
32 | 31 | eleq2d 2820 |
. . . . . . . 8
β’ (π₯ = (ββπ¦) β (π¦ β (π₯(,)(π₯ + 1)) β π¦ β ((ββπ¦)(,)((ββπ¦) + 1)))) |
33 | 32 | rspcev 3613 |
. . . . . . 7
β’
(((ββπ¦)
β β€ β§ π¦
β ((ββπ¦)(,)((ββπ¦) + 1))) β βπ₯ β β€ π¦ β (π₯(,)(π₯ + 1))) |
34 | 11, 28, 33 | syl2anc 585 |
. . . . . 6
β’ (π¦ β (β β
β€) β βπ₯
β β€ π¦ β
(π₯(,)(π₯ + 1))) |
35 | 9, 34 | impbii 208 |
. . . . 5
β’
(βπ₯ β
β€ π¦ β (π₯(,)(π₯ + 1)) β π¦ β (β β
β€)) |
36 | 1, 35 | bitri 275 |
. . . 4
β’ (π¦ β βͺ π₯ β β€ (π₯(,)(π₯ + 1)) β π¦ β (β β
β€)) |
37 | 36 | eqriv 2730 |
. . 3
β’ βͺ π₯ β β€ (π₯(,)(π₯ + 1)) = (β β
β€) |
38 | | zcld.1 |
. . . . 5
β’ π½ = (topGenβran
(,)) |
39 | | retop 24278 |
. . . . 5
β’
(topGenβran (,)) β Top |
40 | 38, 39 | eqeltri 2830 |
. . . 4
β’ π½ β Top |
41 | | iooretop 24282 |
. . . . . 6
β’ (π₯(,)(π₯ + 1)) β (topGenβran
(,)) |
42 | 41, 38 | eleqtrri 2833 |
. . . . 5
β’ (π₯(,)(π₯ + 1)) β π½ |
43 | 42 | rgenw 3066 |
. . . 4
β’
βπ₯ β
β€ (π₯(,)(π₯ + 1)) β π½ |
44 | | iunopn 22400 |
. . . 4
β’ ((π½ β Top β§ βπ₯ β β€ (π₯(,)(π₯ + 1)) β π½) β βͺ
π₯ β β€ (π₯(,)(π₯ + 1)) β π½) |
45 | 40, 43, 44 | mp2an 691 |
. . 3
β’ βͺ π₯ β β€ (π₯(,)(π₯ + 1)) β π½ |
46 | 37, 45 | eqeltrri 2831 |
. 2
β’ (β
β β€) β π½ |
47 | | zssre 12565 |
. . 3
β’ β€
β β |
48 | | uniretop 24279 |
. . . . 5
β’ β =
βͺ (topGenβran (,)) |
49 | 38 | unieqi 4922 |
. . . . 5
β’ βͺ π½ =
βͺ (topGenβran (,)) |
50 | 48, 49 | eqtr4i 2764 |
. . . 4
β’ β =
βͺ π½ |
51 | 50 | iscld2 22532 |
. . 3
β’ ((π½ β Top β§ β€
β β) β (β€ β (Clsdβπ½) β (β β β€) β
π½)) |
52 | 40, 47, 51 | mp2an 691 |
. 2
β’ (β€
β (Clsdβπ½)
β (β β β€) β π½) |
53 | 46, 52 | mpbir 230 |
1
β’ β€
β (Clsdβπ½) |