Step | Hyp | Ref
| Expression |
1 | | mnfxr 11222 |
. . . . . . 7
β’ -β
β β* |
2 | 1 | a1i 11 |
. . . . . 6
β’ (π΄ β β β -β
β β*) |
3 | | rexr 11211 |
. . . . . 6
β’ (π΄ β β β π΄ β
β*) |
4 | | pnfxr 11219 |
. . . . . . 7
β’ +β
β β* |
5 | 4 | a1i 11 |
. . . . . 6
β’ (π΄ β β β +β
β β*) |
6 | | mnflt 13054 |
. . . . . 6
β’ (π΄ β β β -β
< π΄) |
7 | | ltpnf 13051 |
. . . . . 6
β’ (π΄ β β β π΄ < +β) |
8 | | df-ioc 13280 |
. . . . . . 7
β’ (,] =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ β€ π¦)}) |
9 | | df-ioo 13279 |
. . . . . . 7
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
10 | | xrltnle 11232 |
. . . . . . 7
β’ ((π΄ β β*
β§ π€ β
β*) β (π΄ < π€ β Β¬ π€ β€ π΄)) |
11 | | xrlelttr 13086 |
. . . . . . 7
β’ ((π€ β β*
β§ π΄ β
β* β§ +β β β*) β ((π€ β€ π΄ β§ π΄ < +β) β π€ < +β)) |
12 | | xrlttr 13070 |
. . . . . . 7
β’
((-β β β* β§ π΄ β β* β§ π€ β β*)
β ((-β < π΄
β§ π΄ < π€) β -β < π€)) |
13 | 8, 9, 10, 9, 11, 12 | ixxun 13291 |
. . . . . 6
β’
(((-β β β* β§ π΄ β β* β§ +β
β β*) β§ (-β < π΄ β§ π΄ < +β)) β ((-β(,]π΄) βͺ (π΄(,)+β)) =
(-β(,)+β)) |
14 | 2, 3, 5, 6, 7, 13 | syl32anc 1379 |
. . . . 5
β’ (π΄ β β β
((-β(,]π΄) βͺ
(π΄(,)+β)) =
(-β(,)+β)) |
15 | | ioomax 13350 |
. . . . 5
β’
(-β(,)+β) = β |
16 | 14, 15 | eqtrdi 2788 |
. . . 4
β’ (π΄ β β β
((-β(,]π΄) βͺ
(π΄(,)+β)) =
β) |
17 | | iocssre 13355 |
. . . . . 6
β’
((-β β β* β§ π΄ β β) β (-β(,]π΄) β
β) |
18 | 1, 17 | mpan 689 |
. . . . 5
β’ (π΄ β β β
(-β(,]π΄) β
β) |
19 | 8, 9, 10 | ixxdisj 13290 |
. . . . . 6
β’
((-β β β* β§ π΄ β β* β§ +β
β β*) β ((-β(,]π΄) β© (π΄(,)+β)) = β
) |
20 | 1, 3, 5, 19 | mp3an2i 1467 |
. . . . 5
β’ (π΄ β β β
((-β(,]π΄) β©
(π΄(,)+β)) =
β
) |
21 | | uneqdifeq 4456 |
. . . . 5
β’
(((-β(,]π΄)
β β β§ ((-β(,]π΄) β© (π΄(,)+β)) = β
) β
(((-β(,]π΄) βͺ
(π΄(,)+β)) = β
β (β β (-β(,]π΄)) = (π΄(,)+β))) |
22 | 18, 20, 21 | syl2anc 585 |
. . . 4
β’ (π΄ β β β
(((-β(,]π΄) βͺ
(π΄(,)+β)) = β
β (β β (-β(,]π΄)) = (π΄(,)+β))) |
23 | 16, 22 | mpbid 231 |
. . 3
β’ (π΄ β β β (β
β (-β(,]π΄)) =
(π΄(,)+β)) |
24 | | iooretop 24167 |
. . 3
β’ (π΄(,)+β) β
(topGenβran (,)) |
25 | 23, 24 | eqeltrdi 2841 |
. 2
β’ (π΄ β β β (β
β (-β(,]π΄))
β (topGenβran (,))) |
26 | | retop 24163 |
. . 3
β’
(topGenβran (,)) β Top |
27 | | uniretop 24164 |
. . . 4
β’ β =
βͺ (topGenβran (,)) |
28 | 27 | iscld2 22417 |
. . 3
β’
(((topGenβran (,)) β Top β§ (-β(,]π΄) β β) β ((-β(,]π΄) β
(Clsdβ(topGenβran (,))) β (β β (-β(,]π΄)) β (topGenβran
(,)))) |
29 | 26, 18, 28 | sylancr 588 |
. 2
β’ (π΄ β β β
((-β(,]π΄) β
(Clsdβ(topGenβran (,))) β (β β (-β(,]π΄)) β (topGenβran
(,)))) |
30 | 25, 29 | mpbird 257 |
1
β’ (π΄ β β β
(-β(,]π΄) β
(Clsdβ(topGenβran (,)))) |