Step | Hyp | Ref
| Expression |
1 | | limciccioolb.4 |
. 2
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
2 | | ioossicc 13351 |
. . 3
β’ (π΄(,)π΅) β (π΄[,]π΅) |
3 | 2 | a1i 11 |
. 2
β’ (π β (π΄(,)π΅) β (π΄[,]π΅)) |
4 | | limciccioolb.1 |
. . . 4
β’ (π β π΄ β β) |
5 | | limciccioolb.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 | 5 | rexrd 11206 |
. . . . . . . . . . 11
β’ (π β π΅ β
β*) |
14 | | icossre 13346 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β*)
β (π΄[,)π΅) β
β) |
15 | 4, 13, 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 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (-β(,)π΅)) β§ π΄ β€ π₯) β π΄ β€ π₯) |
23 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (-β(,)π΅)) β π₯ β (-β(,)π΅)) |
24 | | mnfxr 11213 |
. . . . . . . . . . . . . . . . . . 19
β’ -β
β β* |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (-β(,)π΅)) β -β β
β*) |
26 | 13 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (-β(,)π΅)) β π΅ β
β*) |
27 | | elioo2 13306 |
. . . . . . . . . . . . . . . . . 18
β’
((-β β β* β§ π΅ β β*) β (π₯ β (-β(,)π΅) β (π₯ β β β§ -β < π₯ β§ π₯ < π΅))) |
28 | 25, 26, 27 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (-β(,)π΅)) β (π₯ β (-β(,)π΅) β (π₯ β β β§ -β < π₯ β§ π₯ < π΅))) |
29 | 23, 28 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (-β(,)π΅)) β (π₯ β β β§ -β < π₯ β§ π₯ < π΅)) |
30 | 29 | simp3d 1145 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (-β(,)π΅)) β π₯ < π΅) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (-β(,)π΅)) β§ π΄ β€ π₯) β π₯ < π΅) |
32 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (-β(,)π΅)) β§ π΄ β€ π₯) β π΄ β β) |
33 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (-β(,)π΅)) β§ π΄ β€ π₯) β π΅ β
β*) |
34 | | elico2 13329 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β*)
β (π₯ β (π΄[,)π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ < π΅))) |
35 | 32, 33, 34 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (-β(,)π΅)) β§ π΄ β€ π₯) β (π₯ β (π΄[,)π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ < π΅))) |
36 | 21, 22, 31, 35 | mpbir3and 1343 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (-β(,)π΅)) β§ π΄ β€ π₯) β π₯ β (π΄[,)π΅)) |
37 | 36 | orcd 872 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (-β(,)π΅)) β§ π΄ β€ π₯) β (π₯ β (π΄[,)π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
38 | 20 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β π₯ β β) |
39 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β Β¬ π΄ β€ π₯) |
40 | 39 | intnanrd 491 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β Β¬ (π΄ β€ π₯ β§ π₯ β€ π΅)) |
41 | 4 | rexrd 11206 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β
β*) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β π΄ β
β*) |
43 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β π΅ β
β*) |
44 | 38 | rexrd 11206 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β π₯ β β*) |
45 | | elicc4 13332 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β β*) β (π₯ β (π΄[,]π΅) β (π΄ β€ π₯ β§ π₯ β€ π΅))) |
46 | 42, 43, 44, 45 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β (π₯ β (π΄[,]π΅) β (π΄ β€ π₯ β§ π₯ β€ π΅))) |
47 | 40, 46 | mtbird 325 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β Β¬ π₯ β (π΄[,]π΅)) |
48 | 38, 47 | eldifd 3922 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β π₯ β (β β (π΄[,]π΅))) |
49 | 48 | olcd 873 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (-β(,)π΅)) β§ Β¬ π΄ β€ π₯) β (π₯ β (π΄[,)π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
50 | 37, 49 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (-β(,)π΅)) β (π₯ β (π΄[,)π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
51 | | elun 4109 |
. . . . . . . . . . 11
β’ (π₯ β ((π΄[,)π΅) βͺ (β β (π΄[,]π΅))) β (π₯ β (π΄[,)π΅) β¨ π₯ β (β β (π΄[,]π΅)))) |
52 | 50, 51 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (-β(,)π΅)) β π₯ β ((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) |
53 | 52 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ₯ β (-β(,)π΅)π₯ β ((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) |
54 | | dfss3 3933 |
. . . . . . . . 9
β’
((-β(,)π΅)
β ((π΄[,)π΅) βͺ (β β (π΄[,]π΅))) β βπ₯ β (-β(,)π΅)π₯ β ((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) |
55 | 53, 54 | sylibr 233 |
. . . . . . . 8
β’ (π β (-β(,)π΅) β ((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) |
56 | | eqid 2737 |
. . . . . . . . 9
β’ βͺ (topGenβran (,)) = βͺ
(topGenβran (,)) |
57 | 56 | ntrss 22409 |
. . . . . . . 8
β’
(((topGenβran (,)) β Top β§ ((π΄[,)π΅) βͺ (β β (π΄[,]π΅))) β βͺ
(topGenβran (,)) β§ (-β(,)π΅) β ((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) β ((intβ(topGenβran
(,)))β(-β(,)π΅))
β ((intβ(topGenβran (,)))β((π΄[,)π΅) βͺ (β β (π΄[,]π΅))))) |
58 | 12, 19, 55, 57 | syl3anc 1372 |
. . . . . . 7
β’ (π β
((intβ(topGenβran (,)))β(-β(,)π΅)) β ((intβ(topGenβran
(,)))β((π΄[,)π΅) βͺ (β β (π΄[,]π΅))))) |
59 | 24 | a1i 11 |
. . . . . . . . 9
β’ (π β -β β
β*) |
60 | 4 | mnfltd 13046 |
. . . . . . . . 9
β’ (π β -β < π΄) |
61 | | limciccioolb.3 |
. . . . . . . . 9
β’ (π β π΄ < π΅) |
62 | 59, 13, 4, 60, 61 | eliood 43743 |
. . . . . . . 8
β’ (π β π΄ β (-β(,)π΅)) |
63 | | iooretop 24132 |
. . . . . . . . . 10
β’
(-β(,)π΅)
β (topGenβran (,)) |
64 | 63 | a1i 11 |
. . . . . . . . 9
β’ (π β (-β(,)π΅) β (topGenβran
(,))) |
65 | | isopn3i 22436 |
. . . . . . . . 9
β’
(((topGenβran (,)) β Top β§ (-β(,)π΅) β (topGenβran (,))) β
((intβ(topGenβran (,)))β(-β(,)π΅)) = (-β(,)π΅)) |
66 | 12, 64, 65 | syl2anc 585 |
. . . . . . . 8
β’ (π β
((intβ(topGenβran (,)))β(-β(,)π΅)) = (-β(,)π΅)) |
67 | 62, 66 | eleqtrrd 2841 |
. . . . . . 7
β’ (π β π΄ β ((intβ(topGenβran
(,)))β(-β(,)π΅))) |
68 | 58, 67 | sseldd 3946 |
. . . . . 6
β’ (π β π΄ β ((intβ(topGenβran
(,)))β((π΄[,)π΅) βͺ (β β (π΄[,]π΅))))) |
69 | 4 | leidd 11722 |
. . . . . . 7
β’ (π β π΄ β€ π΄) |
70 | 4, 5, 61 | ltled 11304 |
. . . . . . 7
β’ (π β π΄ β€ π΅) |
71 | 4, 5, 4, 69, 70 | eliccd 43749 |
. . . . . 6
β’ (π β π΄ β (π΄[,]π΅)) |
72 | 68, 71 | elind 4155 |
. . . . 5
β’ (π β π΄ β (((intβ(topGenβran
(,)))β((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) β© (π΄[,]π΅))) |
73 | | icossicc 13354 |
. . . . . . 7
β’ (π΄[,)π΅) β (π΄[,]π΅) |
74 | 73 | a1i 11 |
. . . . . 6
β’ (π β (π΄[,)π΅) β (π΄[,]π΅)) |
75 | | eqid 2737 |
. . . . . . 7
β’
((topGenβran (,)) βΎt (π΄[,]π΅)) = ((topGenβran (,))
βΎt (π΄[,]π΅)) |
76 | 18, 75 | restntr 22536 |
. . . . . 6
β’
(((topGenβran (,)) β Top β§ (π΄[,]π΅) β β β§ (π΄[,)π΅) β (π΄[,]π΅)) β ((intβ((topGenβran
(,)) βΎt (π΄[,]π΅)))β(π΄[,)π΅)) = (((intβ(topGenβran
(,)))β((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) β© (π΄[,]π΅))) |
77 | 12, 6, 74, 76 | syl3anc 1372 |
. . . . 5
β’ (π β
((intβ((topGenβran (,)) βΎt (π΄[,]π΅)))β(π΄[,)π΅)) = (((intβ(topGenβran
(,)))β((π΄[,)π΅) βͺ (β β (π΄[,]π΅)))) β© (π΄[,]π΅))) |
78 | 72, 77 | eleqtrrd 2841 |
. . . 4
β’ (π β π΄ β ((intβ((topGenβran (,))
βΎt (π΄[,]π΅)))β(π΄[,)π΅))) |
79 | | eqid 2737 |
. . . . . . . . 9
β’
(topGenβran (,)) = (topGenβran (,)) |
80 | 9, 79 | rerest 24170 |
. . . . . . . 8
β’ ((π΄[,]π΅) β β β
((TopOpenββfld) βΎt (π΄[,]π΅)) = ((topGenβran (,))
βΎt (π΄[,]π΅))) |
81 | 6, 80 | syl 17 |
. . . . . . 7
β’ (π β
((TopOpenββfld) βΎt (π΄[,]π΅)) = ((topGenβran (,))
βΎt (π΄[,]π΅))) |
82 | 81 | eqcomd 2743 |
. . . . . 6
β’ (π β ((topGenβran (,))
βΎt (π΄[,]π΅)) = ((TopOpenββfld)
βΎt (π΄[,]π΅))) |
83 | 82 | fveq2d 6847 |
. . . . 5
β’ (π β
(intβ((topGenβran (,)) βΎt (π΄[,]π΅))) =
(intβ((TopOpenββfld) βΎt (π΄[,]π΅)))) |
84 | 83 | fveq1d 6845 |
. . . 4
β’ (π β
((intβ((topGenβran (,)) βΎt (π΄[,]π΅)))β(π΄[,)π΅)) =
((intβ((TopOpenββfld) βΎt (π΄[,]π΅)))β(π΄[,)π΅))) |
85 | 78, 84 | eleqtrd 2840 |
. . 3
β’ (π β π΄ β
((intβ((TopOpenββfld) βΎt (π΄[,]π΅)))β(π΄[,)π΅))) |
86 | 71 | snssd 4770 |
. . . . . . . 8
β’ (π β {π΄} β (π΄[,]π΅)) |
87 | | ssequn2 4144 |
. . . . . . . 8
β’ ({π΄} β (π΄[,]π΅) β ((π΄[,]π΅) βͺ {π΄}) = (π΄[,]π΅)) |
88 | 86, 87 | sylib 217 |
. . . . . . 7
β’ (π β ((π΄[,]π΅) βͺ {π΄}) = (π΄[,]π΅)) |
89 | 88 | eqcomd 2743 |
. . . . . 6
β’ (π β (π΄[,]π΅) = ((π΄[,]π΅) βͺ {π΄})) |
90 | 89 | oveq2d 7374 |
. . . . 5
β’ (π β
((TopOpenββfld) βΎt (π΄[,]π΅)) = ((TopOpenββfld)
βΎt ((π΄[,]π΅) βͺ {π΄}))) |
91 | 90 | fveq2d 6847 |
. . . 4
β’ (π β
(intβ((TopOpenββfld) βΎt (π΄[,]π΅))) =
(intβ((TopOpenββfld) βΎt ((π΄[,]π΅) βͺ {π΄})))) |
92 | | uncom 4114 |
. . . . 5
β’ ((π΄(,)π΅) βͺ {π΄}) = ({π΄} βͺ (π΄(,)π΅)) |
93 | | snunioo 13396 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β ({π΄} βͺ (π΄(,)π΅)) = (π΄[,)π΅)) |
94 | 41, 13, 61, 93 | syl3anc 1372 |
. . . . 5
β’ (π β ({π΄} βͺ (π΄(,)π΅)) = (π΄[,)π΅)) |
95 | 92, 94 | eqtr2id 2790 |
. . . 4
β’ (π β (π΄[,)π΅) = ((π΄(,)π΅) βͺ {π΄})) |
96 | 91, 95 | fveq12d 6850 |
. . 3
β’ (π β
((intβ((TopOpenββfld) βΎt (π΄[,]π΅)))β(π΄[,)π΅)) =
((intβ((TopOpenββfld) βΎt ((π΄[,]π΅) βͺ {π΄})))β((π΄(,)π΅) βͺ {π΄}))) |
97 | 85, 96 | eleqtrd 2840 |
. 2
β’ (π β π΄ β
((intβ((TopOpenββfld) βΎt ((π΄[,]π΅) βͺ {π΄})))β((π΄(,)π΅) βͺ {π΄}))) |
98 | 1, 3, 8, 9, 10, 97 | limcres 25253 |
1
β’ (π β ((πΉ βΎ (π΄(,)π΅)) limβ π΄) = (πΉ limβ π΄)) |