Step | Hyp | Ref
| Expression |
1 | | limcresiooub.d |
. . . . . 6
β’ (π β π· β
β*) |
2 | | limcresiooub.cled |
. . . . . 6
β’ (π β π· β€ π΅) |
3 | | iooss1 13300 |
. . . . . 6
β’ ((π· β β*
β§ π· β€ π΅) β (π΅(,)πΆ) β (π·(,)πΆ)) |
4 | 1, 2, 3 | syl2anc 585 |
. . . . 5
β’ (π β (π΅(,)πΆ) β (π·(,)πΆ)) |
5 | 4 | resabs1d 5969 |
. . . 4
β’ (π β ((πΉ βΎ (π·(,)πΆ)) βΎ (π΅(,)πΆ)) = (πΉ βΎ (π΅(,)πΆ))) |
6 | 5 | eqcomd 2743 |
. . 3
β’ (π β (πΉ βΎ (π΅(,)πΆ)) = ((πΉ βΎ (π·(,)πΆ)) βΎ (π΅(,)πΆ))) |
7 | 6 | oveq1d 7373 |
. 2
β’ (π β ((πΉ βΎ (π΅(,)πΆ)) limβ πΆ) = (((πΉ βΎ (π·(,)πΆ)) βΎ (π΅(,)πΆ)) limβ πΆ)) |
8 | | limcresiooub.f |
. . . 4
β’ (π β πΉ:π΄βΆβ) |
9 | | fresin 6712 |
. . . 4
β’ (πΉ:π΄βΆβ β (πΉ βΎ (π·(,)πΆ)):(π΄ β© (π·(,)πΆ))βΆβ) |
10 | 8, 9 | syl 17 |
. . 3
β’ (π β (πΉ βΎ (π·(,)πΆ)):(π΄ β© (π·(,)πΆ))βΆβ) |
11 | | limcresiooub.bcss |
. . . 4
β’ (π β (π΅(,)πΆ) β π΄) |
12 | 11, 4 | ssind 4193 |
. . 3
β’ (π β (π΅(,)πΆ) β (π΄ β© (π·(,)πΆ))) |
13 | | inss2 4190 |
. . . . 5
β’ (π΄ β© (π·(,)πΆ)) β (π·(,)πΆ) |
14 | | ioosscn 13327 |
. . . . 5
β’ (π·(,)πΆ) β β |
15 | 13, 14 | sstri 3954 |
. . . 4
β’ (π΄ β© (π·(,)πΆ)) β β |
16 | 15 | a1i 11 |
. . 3
β’ (π β (π΄ β© (π·(,)πΆ)) β β) |
17 | | eqid 2737 |
. . 3
β’
(TopOpenββfld) =
(TopOpenββfld) |
18 | | eqid 2737 |
. . 3
β’
((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) = ((TopOpenββfld)
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ})) |
19 | | limcresiooub.b |
. . . . 5
β’ (π β π΅ β
β*) |
20 | | limcresiooub.c |
. . . . . 6
β’ (π β πΆ β β) |
21 | 20 | rexrd 11206 |
. . . . 5
β’ (π β πΆ β
β*) |
22 | | limcresiooub.bltc |
. . . . 5
β’ (π β π΅ < πΆ) |
23 | | ubioc1 13318 |
. . . . 5
β’ ((π΅ β β*
β§ πΆ β
β* β§ π΅
< πΆ) β πΆ β (π΅(,]πΆ)) |
24 | 19, 21, 22, 23 | syl3anc 1372 |
. . . 4
β’ (π β πΆ β (π΅(,]πΆ)) |
25 | | ioounsn 13395 |
. . . . . . 7
β’ ((π΅ β β*
β§ πΆ β
β* β§ π΅
< πΆ) β ((π΅(,)πΆ) βͺ {πΆ}) = (π΅(,]πΆ)) |
26 | 19, 21, 22, 25 | syl3anc 1372 |
. . . . . 6
β’ (π β ((π΅(,)πΆ) βͺ {πΆ}) = (π΅(,]πΆ)) |
27 | 26 | fveq2d 6847 |
. . . . 5
β’ (π β
((intβ((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))β((π΅(,)πΆ) βͺ {πΆ})) =
((intβ((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))β(π΅(,]πΆ))) |
28 | 17 | cnfldtop 24150 |
. . . . . . . 8
β’
(TopOpenββfld) β Top |
29 | | ovex 7391 |
. . . . . . . . . 10
β’ (π·(,)πΆ) β V |
30 | 29 | inex2 5276 |
. . . . . . . . 9
β’ (π΄ β© (π·(,)πΆ)) β V |
31 | | snex 5389 |
. . . . . . . . 9
β’ {πΆ} β V |
32 | 30, 31 | unex 7681 |
. . . . . . . 8
β’ ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β V |
33 | | resttop 22514 |
. . . . . . . 8
β’
(((TopOpenββfld) β Top β§ ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β V) β
((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β Top) |
34 | 28, 32, 33 | mp2an 691 |
. . . . . . 7
β’
((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β Top |
35 | 34 | a1i 11 |
. . . . . 6
β’ (π β
((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β Top) |
36 | | pnfxr 11210 |
. . . . . . . . . . . . . 14
β’ +β
β β* |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β +β β
β*) |
38 | 19 | xrleidd 13072 |
. . . . . . . . . . . . 13
β’ (π β π΅ β€ π΅) |
39 | 20 | ltpnfd 13043 |
. . . . . . . . . . . . 13
β’ (π β πΆ < +β) |
40 | | iocssioo 13357 |
. . . . . . . . . . . . 13
β’ (((π΅ β β*
β§ +β β β*) β§ (π΅ β€ π΅ β§ πΆ < +β)) β (π΅(,]πΆ) β (π΅(,)+β)) |
41 | 19, 37, 38, 39, 40 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (π β (π΅(,]πΆ) β (π΅(,)+β)) |
42 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ = πΆ) β π₯ = πΆ) |
43 | | snidg 4621 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΆ β β β πΆ β {πΆ}) |
44 | | elun2 4138 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΆ β {πΆ} β πΆ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
45 | 20, 43, 44 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΆ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ = πΆ) β πΆ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
47 | 42, 46 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ = πΆ) β π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
48 | 47 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ π₯ = πΆ) β π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
49 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π) |
50 | 19 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (π΅(,]πΆ)) β π΅ β
β*) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π΅ β
β*) |
52 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (π΅(,]πΆ)) β πΆ β
β*) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β πΆ β
β*) |
54 | | iocssre 13345 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β β*
β§ πΆ β β)
β (π΅(,]πΆ) β
β) |
55 | 19, 20, 54 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π΅(,]πΆ) β β) |
56 | 55 | sselda 3945 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (π΅(,]πΆ)) β π₯ β β) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π₯ β β) |
58 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (π΅(,]πΆ)) β π₯ β (π΅(,]πΆ)) |
59 | | iocgtlb 43747 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅ β β*
β§ πΆ β
β* β§ π₯
β (π΅(,]πΆ)) β π΅ < π₯) |
60 | 50, 52, 58, 59 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (π΅(,]πΆ)) β π΅ < π₯) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π΅ < π₯) |
62 | 20 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β πΆ β β) |
63 | | iocleub 43748 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β β*
β§ πΆ β
β* β§ π₯
β (π΅(,]πΆ)) β π₯ β€ πΆ) |
64 | 50, 52, 58, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (π΅(,]πΆ)) β π₯ β€ πΆ) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π₯ β€ πΆ) |
66 | | neqne 2952 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π₯ = πΆ β π₯ β πΆ) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π₯ β πΆ) |
68 | 67 | necomd 3000 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β πΆ β π₯) |
69 | 57, 62, 65, 68 | leneltd 11310 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π₯ < πΆ) |
70 | 51, 53, 57, 61, 69 | eliood 43743 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π₯ β (π΅(,)πΆ)) |
71 | 12 | sselda 3945 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π₯ β (π΄ β© (π·(,)πΆ))) |
72 | | elun1 4137 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄ β© (π·(,)πΆ)) β π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
74 | 49, 70, 73 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π΅(,]πΆ)) β§ Β¬ π₯ = πΆ) β π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
75 | 48, 74 | pm2.61dan 812 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΅(,]πΆ)) β π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
76 | 75 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ (π β βπ₯ β (π΅(,]πΆ)π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
77 | | dfss3 3933 |
. . . . . . . . . . . . 13
β’ ((π΅(,]πΆ) β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β βπ₯ β (π΅(,]πΆ)π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
78 | 76, 77 | sylibr 233 |
. . . . . . . . . . . 12
β’ (π β (π΅(,]πΆ) β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
79 | 41, 78 | ssind 4193 |
. . . . . . . . . . 11
β’ (π β (π΅(,]πΆ) β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) |
80 | 79 | sseld 3944 |
. . . . . . . . . 10
β’ (π β (π₯ β (π΅(,]πΆ) β π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))) |
81 | 24 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ = πΆ) β πΆ β (π΅(,]πΆ)) |
82 | 42, 81 | eqeltrd 2838 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ = πΆ) β π₯ β (π΅(,]πΆ)) |
83 | 82 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ π₯ = πΆ) β π₯ β (π΅(,]πΆ)) |
84 | | ioossioc 43737 |
. . . . . . . . . . . . 13
β’ (π΅(,)πΆ) β (π΅(,]πΆ) |
85 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π΅ β
β*) |
86 | 21 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β πΆ β
β*) |
87 | | elinel1 4156 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β π₯ β (π΅(,)+β)) |
88 | 87 | elioored 43794 |
. . . . . . . . . . . . . . 15
β’ (π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β π₯ β β) |
89 | 88 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π₯ β β) |
90 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β +β β
β*) |
91 | 87 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π₯ β (π΅(,)+β)) |
92 | | ioogtlb 43740 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β β*
β§ +β β β* β§ π₯ β (π΅(,)+β)) β π΅ < π₯) |
93 | 85, 90, 91, 92 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π΅ < π₯) |
94 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π· β
β*) |
95 | | elinel2 4157 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) |
96 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
π₯ = πΆ β Β¬ π₯ = πΆ) |
97 | | velsn 4603 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β {πΆ} β π₯ = πΆ) |
98 | 96, 97 | sylnibr 329 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
π₯ = πΆ β Β¬ π₯ β {πΆ}) |
99 | | elunnel2 4111 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β§ Β¬ π₯ β {πΆ}) β π₯ β (π΄ β© (π·(,)πΆ))) |
100 | 95, 98, 99 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β§ Β¬ π₯ = πΆ) β π₯ β (π΄ β© (π·(,)πΆ))) |
101 | 13, 100 | sselid 3943 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β§ Β¬ π₯ = πΆ) β π₯ β (π·(,)πΆ)) |
102 | 101 | adantll 713 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π₯ β (π·(,)πΆ)) |
103 | | iooltub 43755 |
. . . . . . . . . . . . . . 15
β’ ((π· β β*
β§ πΆ β
β* β§ π₯
β (π·(,)πΆ)) β π₯ < πΆ) |
104 | 94, 86, 102, 103 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π₯ < πΆ) |
105 | 85, 86, 89, 93, 104 | eliood 43743 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π₯ β (π΅(,)πΆ)) |
106 | 84, 105 | sselid 3943 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β§ Β¬ π₯ = πΆ) β π₯ β (π΅(,]πΆ)) |
107 | 83, 106 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β π₯ β (π΅(,]πΆ)) |
108 | 107 | ex 414 |
. . . . . . . . . 10
β’ (π β (π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β π₯ β (π΅(,]πΆ))) |
109 | 80, 108 | impbid 211 |
. . . . . . . . 9
β’ (π β (π₯ β (π΅(,]πΆ) β π₯ β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))) |
110 | 109 | eqrdv 2735 |
. . . . . . . 8
β’ (π β (π΅(,]πΆ) = ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) |
111 | | retop 24128 |
. . . . . . . . . 10
β’
(topGenβran (,)) β Top |
112 | 111 | a1i 11 |
. . . . . . . . 9
β’ (π β (topGenβran (,))
β Top) |
113 | 32 | a1i 11 |
. . . . . . . . 9
β’ (π β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β V) |
114 | | iooretop 24132 |
. . . . . . . . . 10
β’ (π΅(,)+β) β
(topGenβran (,)) |
115 | 114 | a1i 11 |
. . . . . . . . 9
β’ (π β (π΅(,)+β) β (topGenβran
(,))) |
116 | | elrestr 17311 |
. . . . . . . . 9
β’
(((topGenβran (,)) β Top β§ ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β V β§ (π΅(,)+β) β (topGenβran (,)))
β ((π΅(,)+β)
β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β ((topGenβran (,))
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ}))) |
117 | 112, 113,
115, 116 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((π΅(,)+β) β© ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β ((topGenβran (,))
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ}))) |
118 | 110, 117 | eqeltrd 2838 |
. . . . . . 7
β’ (π β (π΅(,]πΆ) β ((topGenβran (,))
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ}))) |
119 | 17 | tgioo2 24169 |
. . . . . . . . 9
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
120 | 119 | oveq1i 7368 |
. . . . . . . 8
β’
((topGenβran (,)) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) =
(((TopOpenββfld) βΎt β)
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ})) |
121 | 28 | a1i 11 |
. . . . . . . . 9
β’ (π β
(TopOpenββfld) β Top) |
122 | | ioossre 13326 |
. . . . . . . . . . . 12
β’ (π·(,)πΆ) β β |
123 | 13, 122 | sstri 3954 |
. . . . . . . . . . 11
β’ (π΄ β© (π·(,)πΆ)) β β |
124 | 123 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π΄ β© (π·(,)πΆ)) β β) |
125 | 20 | snssd 4770 |
. . . . . . . . . 10
β’ (π β {πΆ} β β) |
126 | 124, 125 | unssd 4147 |
. . . . . . . . 9
β’ (π β ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β β) |
127 | | reex 11143 |
. . . . . . . . . 10
β’ β
β V |
128 | 127 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
V) |
129 | | restabs 22519 |
. . . . . . . . 9
β’
(((TopOpenββfld) β Top β§ ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}) β β β§ β β V)
β (((TopOpenββfld) βΎt β)
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ})) = ((TopOpenββfld)
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ}))) |
130 | 121, 126,
128, 129 | syl3anc 1372 |
. . . . . . . 8
β’ (π β
(((TopOpenββfld) βΎt β)
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ})) = ((TopOpenββfld)
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ}))) |
131 | 120, 130 | eqtrid 2789 |
. . . . . . 7
β’ (π β ((topGenβran (,))
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ})) = ((TopOpenββfld)
βΎt ((π΄
β© (π·(,)πΆ)) βͺ {πΆ}))) |
132 | 118, 131 | eleqtrd 2840 |
. . . . . 6
β’ (π β (π΅(,]πΆ) β
((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) |
133 | | isopn3i 22436 |
. . . . . 6
β’
((((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})) β Top β§ (π΅(,]πΆ) β
((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ}))) β
((intβ((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))β(π΅(,]πΆ)) = (π΅(,]πΆ)) |
134 | 35, 132, 133 | syl2anc 585 |
. . . . 5
β’ (π β
((intβ((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))β(π΅(,]πΆ)) = (π΅(,]πΆ)) |
135 | 27, 134 | eqtr2d 2778 |
. . . 4
β’ (π β (π΅(,]πΆ) =
((intβ((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))β((π΅(,)πΆ) βͺ {πΆ}))) |
136 | 24, 135 | eleqtrd 2840 |
. . 3
β’ (π β πΆ β
((intβ((TopOpenββfld) βΎt ((π΄ β© (π·(,)πΆ)) βͺ {πΆ})))β((π΅(,)πΆ) βͺ {πΆ}))) |
137 | 10, 12, 16, 17, 18, 136 | limcres 25253 |
. 2
β’ (π β (((πΉ βΎ (π·(,)πΆ)) βΎ (π΅(,)πΆ)) limβ πΆ) = ((πΉ βΎ (π·(,)πΆ)) limβ πΆ)) |
138 | 7, 137 | eqtrd 2777 |
1
β’ (π β ((πΉ βΎ (π΅(,)πΆ)) limβ πΆ) = ((πΉ βΎ (π·(,)πΆ)) limβ πΆ)) |