Step | Hyp | Ref
| Expression |
1 | | limcicciooub.4 |
. 2
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
2 | | ioossicc 13351 |
. . 3
β’ (π΄(,)π΅) β (π΄[,]π΅) |
3 | 2 | a1i 11 |
. 2
β’ (π β (π΄(,)π΅) β (π΄[,]π΅)) |
4 | | limcicciooub.1 |
. . . 4
β’ (π β π΄ β β) |
5 | | limcicciooub.2 |
. . . 4
β’ (π β π΅ β β) |
6 | 4, 5 | iccssred 13352 |
. . 3
β’ (π β (π΄[,]π΅) β β) |
7 | | ax-resscn 11109 |
. . 3
β’ β
β β |
8 | 6, 7 | sstrdi 3957 |
. 2
β’ (π β (π΄[,]π΅) β β) |
9 | | eqid 2737 |
. 2
β’
(TopOpenββfld) =
(TopOpenββfld) |
10 | | eqid 2737 |
. 2
β’
((TopOpenββfld) βΎt ((π΄[,]π΅) βͺ {π΅})) = ((TopOpenββfld)
βΎt ((π΄[,]π΅) βͺ {π΅})) |
11 | | retop 24128 |
. . . . . . . . 9
β’
(topGenβran (,)) β Top |
12 | 11 | a1i 11 |
. . . . . . . 8
β’ (π β (topGenβran (,))
β Top) |
13 | 4 | rexrd 11206 |
. . . . . . . . . . 11
β’ (π β π΄ β
β*) |
14 | | iocssre 13345 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ π΅ β β)
β (π΄(,]π΅) β
β) |
15 | 13, 5, 14 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π΄(,]π΅) β β) |
16 | | difssd 4093 |
. . . . . . . . . 10
β’ (π β (β β (π΄[,]π΅)) β β) |
17 | 15, 16 | unssd 4147 |
. . . . . . . . 9
β’ (π β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅))) β β) |
18 | | uniretop 24129 |
. . . . . . . . 9
β’ β =
βͺ (topGenβran (,)) |
19 | 17, 18 | sseqtrdi 3995 |
. . . . . . . 8
β’ (π β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅))) β βͺ
(topGenβran (,))) |
20 | | elioore 13295 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄(,)+β) β π₯ β β) |
21 | 20 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β π₯ β β) |
22 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β π₯ β (π΄(,)+β)) |
23 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β π΄ β
β*) |
24 | | pnfxr 11210 |
. . . . . . . . . . . . . . . . 17
β’ +β
β β* |
25 | | elioo2 13306 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β*
β§ +β β β*) β (π₯ β (π΄(,)+β) β (π₯ β β β§ π΄ < π₯ β§ π₯ < +β))) |
26 | 23, 24, 25 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β (π₯ β (π΄(,)+β) β (π₯ β β β§ π΄ < π₯ β§ π₯ < +β))) |
27 | 22, 26 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β (π₯ β β β§ π΄ < π₯ β§ π₯ < +β)) |
28 | 27 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β π΄ < π₯) |
29 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β π₯ β€ π΅) |
30 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β π΅ β β) |
31 | | elioc2 13328 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β*
β§ π΅ β β)
β (π₯ β (π΄(,]π΅) β (π₯ β β β§ π΄ < π₯ β§ π₯ β€ π΅))) |
32 | 23, 30, 31 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β (π₯ β (π΄(,]π΅) β (π₯ β β β§ π΄ < π₯ β§ π₯ β€ π΅))) |
33 | 21, 28, 29, 32 | mpbir3and 1343 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β π₯ β (π΄(,]π΅)) |
34 | 33 | orcd 872 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π΄(,)+β)) β§ π₯ β€ π΅) β (π₯ β (π΄(,]π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
35 | 20 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β π₯ β β) |
36 | | 3mix3 1333 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π₯ β€ π΅ β (Β¬ π₯ β β β¨ Β¬ π΄ β€ π₯ β¨ Β¬ π₯ β€ π΅)) |
37 | | 3ianor 1108 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
(π₯ β β β§
π΄ β€ π₯ β§ π₯ β€ π΅) β (Β¬ π₯ β β β¨ Β¬ π΄ β€ π₯ β¨ Β¬ π₯ β€ π΅)) |
38 | 36, 37 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π₯ β€ π΅ β Β¬ (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅)) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β Β¬ (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅)) |
40 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β π΄ β β) |
41 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β π΅ β β) |
42 | | elicc2 13330 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ π΅ β β) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
43 | 40, 41, 42 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
44 | 39, 43 | mtbird 325 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β Β¬ π₯ β (π΄[,]π΅)) |
45 | 35, 44 | eldifd 3922 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β π₯ β (β β (π΄[,]π΅))) |
46 | 45 | olcd 873 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π΄(,)+β)) β§ Β¬ π₯ β€ π΅) β (π₯ β (π΄(,]π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
47 | 34, 46 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄(,)+β)) β (π₯ β (π΄(,]π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
48 | | elun 4109 |
. . . . . . . . . . 11
β’ (π₯ β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅))) β (π₯ β (π΄(,]π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
49 | 47, 48 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)+β)) β π₯ β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) |
50 | 49 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ₯ β (π΄(,)+β)π₯ β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) |
51 | | dfss3 3933 |
. . . . . . . . 9
β’ ((π΄(,)+β) β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅))) β βπ₯ β (π΄(,)+β)π₯ β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) |
52 | 50, 51 | sylibr 233 |
. . . . . . . 8
β’ (π β (π΄(,)+β) β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) |
53 | | eqid 2737 |
. . . . . . . . 9
β’ βͺ (topGenβran (,)) = βͺ
(topGenβran (,)) |
54 | 53 | ntrss 22409 |
. . . . . . . 8
β’
(((topGenβran (,)) β Top β§ ((π΄(,]π΅) βͺ (β β (π΄[,]π΅))) β βͺ
(topGenβran (,)) β§ (π΄(,)+β) β ((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) β ((intβ(topGenβran
(,)))β(π΄(,)+β))
β ((intβ(topGenβran (,)))β((π΄(,]π΅) βͺ (β β (π΄[,]π΅))))) |
55 | 12, 19, 52, 54 | syl3anc 1372 |
. . . . . . 7
β’ (π β
((intβ(topGenβran (,)))β(π΄(,)+β)) β
((intβ(topGenβran (,)))β((π΄(,]π΅) βͺ (β β (π΄[,]π΅))))) |
56 | 24 | a1i 11 |
. . . . . . . . 9
β’ (π β +β β
β*) |
57 | | limcicciooub.3 |
. . . . . . . . 9
β’ (π β π΄ < π΅) |
58 | 5 | ltpnfd 13043 |
. . . . . . . . 9
β’ (π β π΅ < +β) |
59 | 13, 56, 5, 57, 58 | eliood 43743 |
. . . . . . . 8
β’ (π β π΅ β (π΄(,)+β)) |
60 | | iooretop 24132 |
. . . . . . . . 9
β’ (π΄(,)+β) β
(topGenβran (,)) |
61 | | isopn3i 22436 |
. . . . . . . . 9
β’
(((topGenβran (,)) β Top β§ (π΄(,)+β) β (topGenβran (,)))
β ((intβ(topGenβran (,)))β(π΄(,)+β)) = (π΄(,)+β)) |
62 | 12, 60, 61 | sylancl 587 |
. . . . . . . 8
β’ (π β
((intβ(topGenβran (,)))β(π΄(,)+β)) = (π΄(,)+β)) |
63 | 59, 62 | eleqtrrd 2841 |
. . . . . . 7
β’ (π β π΅ β ((intβ(topGenβran
(,)))β(π΄(,)+β))) |
64 | 55, 63 | sseldd 3946 |
. . . . . 6
β’ (π β π΅ β ((intβ(topGenβran
(,)))β((π΄(,]π΅) βͺ (β β (π΄[,]π΅))))) |
65 | 5 | rexrd 11206 |
. . . . . . 7
β’ (π β π΅ β
β*) |
66 | 4, 5, 57 | ltled 11304 |
. . . . . . 7
β’ (π β π΄ β€ π΅) |
67 | | ubicc2 13383 |
. . . . . . 7
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΅ β (π΄[,]π΅)) |
68 | 13, 65, 66, 67 | syl3anc 1372 |
. . . . . 6
β’ (π β π΅ β (π΄[,]π΅)) |
69 | 64, 68 | elind 4155 |
. . . . 5
β’ (π β π΅ β (((intβ(topGenβran
(,)))β((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) β© (π΄[,]π΅))) |
70 | | iocssicc 13355 |
. . . . . . 7
β’ (π΄(,]π΅) β (π΄[,]π΅) |
71 | 70 | a1i 11 |
. . . . . 6
β’ (π β (π΄(,]π΅) β (π΄[,]π΅)) |
72 | | eqid 2737 |
. . . . . . 7
β’
((topGenβran (,)) βΎt (π΄[,]π΅)) = ((topGenβran (,))
βΎt (π΄[,]π΅)) |
73 | 18, 72 | restntr 22536 |
. . . . . 6
β’
(((topGenβran (,)) β Top β§ (π΄[,]π΅) β β β§ (π΄(,]π΅) β (π΄[,]π΅)) β ((intβ((topGenβran
(,)) βΎt (π΄[,]π΅)))β(π΄(,]π΅)) = (((intβ(topGenβran
(,)))β((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) β© (π΄[,]π΅))) |
74 | 12, 6, 71, 73 | syl3anc 1372 |
. . . . 5
β’ (π β
((intβ((topGenβran (,)) βΎt (π΄[,]π΅)))β(π΄(,]π΅)) = (((intβ(topGenβran
(,)))β((π΄(,]π΅) βͺ (β β (π΄[,]π΅)))) β© (π΄[,]π΅))) |
75 | 69, 74 | eleqtrrd 2841 |
. . . 4
β’ (π β π΅ β ((intβ((topGenβran (,))
βΎt (π΄[,]π΅)))β(π΄(,]π΅))) |
76 | | eqid 2737 |
. . . . . . . . 9
β’
(topGenβran (,)) = (topGenβran (,)) |
77 | 9, 76 | rerest 24170 |
. . . . . . . 8
β’ ((π΄[,]π΅) β β β
((TopOpenββfld) βΎt (π΄[,]π΅)) = ((topGenβran (,))
βΎt (π΄[,]π΅))) |
78 | 6, 77 | syl 17 |
. . . . . . 7
β’ (π β
((TopOpenββfld) βΎt (π΄[,]π΅)) = ((topGenβran (,))
βΎt (π΄[,]π΅))) |
79 | 78 | eqcomd 2743 |
. . . . . 6
β’ (π β ((topGenβran (,))
βΎt (π΄[,]π΅)) = ((TopOpenββfld)
βΎt (π΄[,]π΅))) |
80 | 79 | fveq2d 6847 |
. . . . 5
β’ (π β
(intβ((topGenβran (,)) βΎt (π΄[,]π΅))) =
(intβ((TopOpenββfld) βΎt (π΄[,]π΅)))) |
81 | 80 | fveq1d 6845 |
. . . 4
β’ (π β
((intβ((topGenβran (,)) βΎt (π΄[,]π΅)))β(π΄(,]π΅)) =
((intβ((TopOpenββfld) βΎt (π΄[,]π΅)))β(π΄(,]π΅))) |
82 | 75, 81 | eleqtrd 2840 |
. . 3
β’ (π β π΅ β
((intβ((TopOpenββfld) βΎt (π΄[,]π΅)))β(π΄(,]π΅))) |
83 | 68 | snssd 4770 |
. . . . . . . 8
β’ (π β {π΅} β (π΄[,]π΅)) |
84 | | ssequn2 4144 |
. . . . . . . 8
β’ ({π΅} β (π΄[,]π΅) β ((π΄[,]π΅) βͺ {π΅}) = (π΄[,]π΅)) |
85 | 83, 84 | sylib 217 |
. . . . . . 7
β’ (π β ((π΄[,]π΅) βͺ {π΅}) = (π΄[,]π΅)) |
86 | 85 | eqcomd 2743 |
. . . . . 6
β’ (π β (π΄[,]π΅) = ((π΄[,]π΅) βͺ {π΅})) |
87 | 86 | oveq2d 7374 |
. . . . 5
β’ (π β
((TopOpenββfld) βΎt (π΄[,]π΅)) = ((TopOpenββfld)
βΎt ((π΄[,]π΅) βͺ {π΅}))) |
88 | 87 | fveq2d 6847 |
. . . 4
β’ (π β
(intβ((TopOpenββfld) βΎt (π΄[,]π΅))) =
(intβ((TopOpenββfld) βΎt ((π΄[,]π΅) βͺ {π΅})))) |
89 | | ioounsn 13395 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β ((π΄(,)π΅) βͺ {π΅}) = (π΄(,]π΅)) |
90 | 13, 65, 57, 89 | syl3anc 1372 |
. . . . 5
β’ (π β ((π΄(,)π΅) βͺ {π΅}) = (π΄(,]π΅)) |
91 | 90 | eqcomd 2743 |
. . . 4
β’ (π β (π΄(,]π΅) = ((π΄(,)π΅) βͺ {π΅})) |
92 | 88, 91 | fveq12d 6850 |
. . 3
β’ (π β
((intβ((TopOpenββfld) βΎt (π΄[,]π΅)))β(π΄(,]π΅)) =
((intβ((TopOpenββfld) βΎt ((π΄[,]π΅) βͺ {π΅})))β((π΄(,)π΅) βͺ {π΅}))) |
93 | 82, 92 | eleqtrd 2840 |
. 2
β’ (π β π΅ β
((intβ((TopOpenββfld) βΎt ((π΄[,]π΅) βͺ {π΅})))β((π΄(,)π΅) βͺ {π΅}))) |
94 | 1, 3, 8, 9, 10, 93 | limcres 25253 |
1
β’ (π β ((πΉ βΎ (π΄(,)π΅)) limβ π΅) = (πΉ limβ π΅)) |