Step | Hyp | Ref
| Expression |
1 | | 0red 11168 |
. . . 4
β’
(((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β§ π¦ < 0) β 0 β
β) |
2 | | simpllr 775 |
. . . 4
β’
(((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β§ Β¬ π¦ < 0) β π¦ β
β) |
3 | 1, 2 | ifclda 4527 |
. . 3
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β if(π¦ < 0, 0, π¦) β β) |
4 | | ovif 7460 |
. . . . . 6
β’ (if(π¦ < 0, 0, π¦)(,]+β) = if(π¦ < 0, (0(,]+β), (π¦(,]+β)) |
5 | | rexr 11211 |
. . . . . . 7
β’ (π¦ β β β π¦ β
β*) |
6 | | 0xr 11212 |
. . . . . . . 8
β’ 0 β
β* |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π¦ β β β 0 β
β*) |
8 | | pnfxr 11219 |
. . . . . . . 8
β’ +β
β β* |
9 | 8 | a1i 11 |
. . . . . . 7
β’ (π¦ β β β +β
β β*) |
10 | | iocinif 31753 |
. . . . . . 7
β’ ((π¦ β β*
β§ 0 β β* β§ +β β β*)
β ((π¦(,]+β)
β© (0(,]+β)) = if(π¦ < 0, (0(,]+β), (π¦(,]+β))) |
11 | 5, 7, 9, 10 | syl3anc 1372 |
. . . . . 6
β’ (π¦ β β β ((π¦(,]+β) β©
(0(,]+β)) = if(π¦ <
0, (0(,]+β), (π¦(,]+β))) |
12 | 4, 11 | eqtr4id 2791 |
. . . . 5
β’ (π¦ β β β (if(π¦ < 0, 0, π¦)(,]+β) = ((π¦(,]+β) β©
(0(,]+β))) |
13 | 12 | ad2antlr 726 |
. . . 4
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β (if(π¦ < 0, 0, π¦)(,]+β) = ((π¦(,]+β) β©
(0(,]+β))) |
14 | | iocssicc 13365 |
. . . . . 6
β’
(0(,]+β) β (0[,]+β) |
15 | | sslin 4200 |
. . . . . 6
β’
((0(,]+β) β (0[,]+β) β ((π¦(,]+β) β© (0(,]+β)) β
((π¦(,]+β) β©
(0[,]+β))) |
16 | 14, 15 | mp1i 13 |
. . . . 5
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β ((π¦(,]+β) β©
(0(,]+β)) β ((π¦(,]+β) β©
(0[,]+β))) |
17 | | simpr 486 |
. . . . . 6
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β (π¦(,]+β) β (π΄ β©
(0(,]+β))) |
18 | | ssin 4196 |
. . . . . . . 8
β’ (((π¦(,]+β) β π΄ β§ (π¦(,]+β) β (0(,]+β)) β
(π¦(,]+β) β
(π΄ β©
(0(,]+β))) |
19 | 18 | biimpri 227 |
. . . . . . 7
β’ ((π¦(,]+β) β (π΄ β© (0(,]+β)) β
((π¦(,]+β) β
π΄ β§ (π¦(,]+β) β
(0(,]+β))) |
20 | 19 | simpld 496 |
. . . . . 6
β’ ((π¦(,]+β) β (π΄ β© (0(,]+β)) β
(π¦(,]+β) β
π΄) |
21 | | ssinss1 4203 |
. . . . . 6
β’ ((π¦(,]+β) β π΄ β ((π¦(,]+β) β© (0[,]+β)) β
π΄) |
22 | 17, 20, 21 | 3syl 18 |
. . . . 5
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β ((π¦(,]+β) β©
(0[,]+β)) β π΄) |
23 | 16, 22 | sstrd 3958 |
. . . 4
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β ((π¦(,]+β) β©
(0(,]+β)) β π΄) |
24 | 13, 23 | eqsstrd 3986 |
. . 3
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β (if(π¦ < 0, 0, π¦)(,]+β) β π΄) |
25 | | oveq1 7370 |
. . . . 5
β’ (π₯ = if(π¦ < 0, 0, π¦) β (π₯(,]+β) = (if(π¦ < 0, 0, π¦)(,]+β)) |
26 | 25 | sseq1d 3979 |
. . . 4
β’ (π₯ = if(π¦ < 0, 0, π¦) β ((π₯(,]+β) β π΄ β (if(π¦ < 0, 0, π¦)(,]+β) β π΄)) |
27 | 26 | rspcev 3583 |
. . 3
β’
((if(π¦ < 0, 0,
π¦) β β β§
(if(π¦ < 0, 0, π¦)(,]+β) β π΄) β βπ₯ β β (π₯(,]+β) β π΄) |
28 | 3, 24, 27 | syl2anc 585 |
. 2
β’ ((((π΄ β π½ β§ +β β π΄) β§ π¦ β β) β§ (π¦(,]+β) β (π΄ β© (0(,]+β))) β βπ₯ β β (π₯(,]+β) β π΄) |
29 | | letopon 22594 |
. . . . . . . . . 10
β’
(ordTopβ β€ ) β
(TopOnββ*) |
30 | | iccssxr 13358 |
. . . . . . . . . 10
β’
(0[,]+β) β β* |
31 | | resttopon 22550 |
. . . . . . . . . 10
β’
(((ordTopβ β€ ) β (TopOnββ*) β§
(0[,]+β) β β*) β ((ordTopβ β€ )
βΎt (0[,]+β)) β
(TopOnβ(0[,]+β))) |
32 | 29, 30, 31 | mp2an 691 |
. . . . . . . . 9
β’
((ordTopβ β€ ) βΎt (0[,]+β)) β
(TopOnβ(0[,]+β)) |
33 | 32 | topontopi 22302 |
. . . . . . . 8
β’
((ordTopβ β€ ) βΎt (0[,]+β)) β
Top |
34 | 33 | a1i 11 |
. . . . . . 7
β’ (π΄ β π½ β ((ordTopβ β€ )
βΎt (0[,]+β)) β Top) |
35 | | ovex 7396 |
. . . . . . . 8
β’
(0(,]+β) β V |
36 | 35 | a1i 11 |
. . . . . . 7
β’ (π΄ β π½ β (0(,]+β) β
V) |
37 | | pnfneige0.j |
. . . . . . . . . 10
β’ π½ =
(TopOpenβ(β*π βΎs
(0[,]+β))) |
38 | | xrge0topn 32614 |
. . . . . . . . . 10
β’
(TopOpenβ(β*π
βΎs (0[,]+β))) = ((ordTopβ β€ )
βΎt (0[,]+β)) |
39 | 37, 38 | eqtri 2760 |
. . . . . . . . 9
β’ π½ = ((ordTopβ β€ )
βΎt (0[,]+β)) |
40 | 39 | eleq2i 2825 |
. . . . . . . 8
β’ (π΄ β π½ β π΄ β ((ordTopβ β€ )
βΎt (0[,]+β))) |
41 | 40 | biimpi 215 |
. . . . . . 7
β’ (π΄ β π½ β π΄ β ((ordTopβ β€ )
βΎt (0[,]+β))) |
42 | | elrestr 17325 |
. . . . . . 7
β’
((((ordTopβ β€ ) βΎt (0[,]+β)) β Top
β§ (0(,]+β) β V β§ π΄ β ((ordTopβ β€ )
βΎt (0[,]+β))) β (π΄ β© (0(,]+β)) β
(((ordTopβ β€ ) βΎt (0[,]+β)) βΎt
(0(,]+β))) |
43 | 34, 36, 41, 42 | syl3anc 1372 |
. . . . . 6
β’ (π΄ β π½ β (π΄ β© (0(,]+β)) β
(((ordTopβ β€ ) βΎt (0[,]+β)) βΎt
(0(,]+β))) |
44 | | letop 22595 |
. . . . . . 7
β’
(ordTopβ β€ ) β Top |
45 | | ovex 7396 |
. . . . . . 7
β’
(0[,]+β) β V |
46 | | restabs 22554 |
. . . . . . 7
β’
(((ordTopβ β€ ) β Top β§ (0(,]+β) β
(0[,]+β) β§ (0[,]+β) β V) β (((ordTopβ β€ )
βΎt (0[,]+β)) βΎt (0(,]+β)) =
((ordTopβ β€ ) βΎt (0(,]+β))) |
47 | 44, 14, 45, 46 | mp3an 1462 |
. . . . . 6
β’
(((ordTopβ β€ ) βΎt (0[,]+β))
βΎt (0(,]+β)) = ((ordTopβ β€ )
βΎt (0(,]+β)) |
48 | 43, 47 | eleqtrdi 2843 |
. . . . 5
β’ (π΄ β π½ β (π΄ β© (0(,]+β)) β
((ordTopβ β€ ) βΎt (0(,]+β))) |
49 | 44 | a1i 11 |
. . . . . 6
β’ (π΄ β π½ β (ordTopβ β€ ) β
Top) |
50 | | iocpnfordt 22604 |
. . . . . . 7
β’
(0(,]+β) β (ordTopβ β€ ) |
51 | 50 | a1i 11 |
. . . . . 6
β’ (π΄ β π½ β (0(,]+β) β (ordTopβ
β€ )) |
52 | | ssidd 3971 |
. . . . . 6
β’ (π΄ β π½ β (0(,]+β) β
(0(,]+β)) |
53 | | inss2 4195 |
. . . . . . 7
β’ (π΄ β© (0(,]+β)) β
(0(,]+β) |
54 | 53 | a1i 11 |
. . . . . 6
β’ (π΄ β π½ β (π΄ β© (0(,]+β)) β
(0(,]+β)) |
55 | | restopnb 22564 |
. . . . . 6
β’
((((ordTopβ β€ ) β Top β§ (0(,]+β) β V) β§
((0(,]+β) β (ordTopβ β€ ) β§ (0(,]+β) β
(0(,]+β) β§ (π΄
β© (0(,]+β)) β (0(,]+β))) β ((π΄ β© (0(,]+β)) β (ordTopβ
β€ ) β (π΄ β©
(0(,]+β)) β ((ordTopβ β€ ) βΎt
(0(,]+β)))) |
56 | 49, 36, 51, 52, 54, 55 | syl23anc 1378 |
. . . . 5
β’ (π΄ β π½ β ((π΄ β© (0(,]+β)) β (ordTopβ
β€ ) β (π΄ β©
(0(,]+β)) β ((ordTopβ β€ ) βΎt
(0(,]+β)))) |
57 | 48, 56 | mpbird 257 |
. . . 4
β’ (π΄ β π½ β (π΄ β© (0(,]+β)) β (ordTopβ
β€ )) |
58 | 57 | adantr 482 |
. . 3
β’ ((π΄ β π½ β§ +β β π΄) β (π΄ β© (0(,]+β)) β (ordTopβ
β€ )) |
59 | | simpr 486 |
. . . 4
β’ ((π΄ β π½ β§ +β β π΄) β +β β π΄) |
60 | | 0ltpnf 13053 |
. . . . . 6
β’ 0 <
+β |
61 | | ubioc1 13328 |
. . . . . 6
β’ ((0
β β* β§ +β β β* β§ 0
< +β) β +β β (0(,]+β)) |
62 | 6, 8, 60, 61 | mp3an 1462 |
. . . . 5
β’ +β
β (0(,]+β) |
63 | 62 | a1i 11 |
. . . 4
β’ ((π΄ β π½ β§ +β β π΄) β +β β
(0(,]+β)) |
64 | 59, 63 | elind 4160 |
. . 3
β’ ((π΄ β π½ β§ +β β π΄) β +β β (π΄ β© (0(,]+β))) |
65 | | pnfnei 22609 |
. . 3
β’ (((π΄ β© (0(,]+β)) β
(ordTopβ β€ ) β§ +β β (π΄ β© (0(,]+β))) β βπ¦ β β (π¦(,]+β) β (π΄ β©
(0(,]+β))) |
66 | 58, 64, 65 | syl2anc 585 |
. 2
β’ ((π΄ β π½ β§ +β β π΄) β βπ¦ β β (π¦(,]+β) β (π΄ β© (0(,]+β))) |
67 | 28, 66 | r19.29a 3156 |
1
β’ ((π΄ β π½ β§ +β β π΄) β βπ₯ β β (π₯(,]+β) β π΄) |