Step | Hyp | Ref
| Expression |
1 | | ellimc3.f |
. . 3
β’ (π β πΉ:π΄βΆβ) |
2 | | ellimc3.a |
. . 3
β’ (π β π΄ β β) |
3 | | ellimc3.b |
. . 3
β’ (π β π΅ β β) |
4 | | eqid 2733 |
. . 3
β’
(TopOpenββfld) =
(TopOpenββfld) |
5 | 1, 2, 3, 4 | ellimc2 25264 |
. 2
β’ (π β (πΆ β (πΉ limβ π΅) β (πΆ β β β§ βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’))))) |
6 | | cnxmet 24159 |
. . . . . . . . 9
β’ (abs
β β ) β (βMetββ) |
7 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ π₯ β β+) β πΆ β
β) |
8 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ π₯ β β+) β π₯ β
β+) |
9 | | blcntr 23789 |
. . . . . . . . 9
β’ (((abs
β β ) β (βMetββ) β§ πΆ β β β§ π₯ β β+) β πΆ β (πΆ(ballβ(abs β β ))π₯)) |
10 | 6, 7, 8, 9 | mp3an2i 1467 |
. . . . . . . 8
β’ (((π β§ πΆ β β) β§ π₯ β β+) β πΆ β (πΆ(ballβ(abs β β ))π₯)) |
11 | | rpxr 12932 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
β*) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β) β§ π₯ β β+) β π₯ β
β*) |
13 | 4 | cnfldtopn 24168 |
. . . . . . . . . . 11
β’
(TopOpenββfld) = (MetOpenβ(abs β
β )) |
14 | 13 | blopn 23879 |
. . . . . . . . . 10
β’ (((abs
β β ) β (βMetββ) β§ πΆ β β β§ π₯ β β*) β (πΆ(ballβ(abs β β
))π₯) β
(TopOpenββfld)) |
15 | 6, 7, 12, 14 | mp3an2i 1467 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ π₯ β β+) β (πΆ(ballβ(abs β β
))π₯) β
(TopOpenββfld)) |
16 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π’ = (πΆ(ballβ(abs β β ))π₯) β (πΆ β π’ β πΆ β (πΆ(ballβ(abs β β ))π₯))) |
17 | | sseq2 3974 |
. . . . . . . . . . . . 13
β’ (π’ = (πΆ(ballβ(abs β β ))π₯) β ((πΉ β (π£ β© (π΄ β {π΅}))) β π’ β (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
18 | 17 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π’ = (πΆ(ballβ(abs β β ))π₯) β ((π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’) β (π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)))) |
19 | 18 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π’ = (πΆ(ballβ(abs β β ))π₯) β (βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)))) |
20 | 16, 19 | imbi12d 345 |
. . . . . . . . . 10
β’ (π’ = (πΆ(ballβ(abs β β ))π₯) β ((πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β (πΆ β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))))) |
21 | 20 | rspcv 3579 |
. . . . . . . . 9
β’ ((πΆ(ballβ(abs β β
))π₯) β
(TopOpenββfld) β (βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β (πΆ β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))))) |
22 | 15, 21 | syl 17 |
. . . . . . . 8
β’ (((π β§ πΆ β β) β§ π₯ β β+) β
(βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β (πΆ β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))))) |
23 | 10, 22 | mpid 44 |
. . . . . . 7
β’ (((π β§ πΆ β β) β§ π₯ β β+) β
(βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)))) |
24 | 13 | mopni2 23872 |
. . . . . . . . . . 11
β’ (((abs
β β ) β (βMetββ) β§ π£ β (TopOpenββfld)
β§ π΅ β π£) β βπ¦ β β+
(π΅(ballβ(abs β
β ))π¦) β π£) |
25 | 6, 24 | mp3an1 1449 |
. . . . . . . . . 10
β’ ((π£ β
(TopOpenββfld) β§ π΅ β π£) β βπ¦ β β+ (π΅(ballβ(abs β β
))π¦) β π£) |
26 | | ssrin 4197 |
. . . . . . . . . . . . 13
β’ ((π΅(ballβ(abs β β
))π¦) β π£ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅})) β (π£ β© (π΄ β {π΅}))) |
27 | | imass2 6058 |
. . . . . . . . . . . . 13
β’ (((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅})) β (π£ β© (π΄ β {π΅})) β (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΉ β (π£ β© (π΄ β {π΅})))) |
28 | | sstr2 3955 |
. . . . . . . . . . . . 13
β’ ((πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΉ β (π£ β© (π΄ β {π΅}))) β ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π΅(ballβ(abs β β
))π¦) β π£ β ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
30 | 29 | com12 32 |
. . . . . . . . . . 11
β’ ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β ((π΅(ballβ(abs β β ))π¦) β π£ β (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
31 | 30 | reximdv 3164 |
. . . . . . . . . 10
β’ ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β (βπ¦ β β+
(π΅(ballβ(abs β
β ))π¦) β π£ β βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
32 | 25, 31 | syl5com 31 |
. . . . . . . . 9
β’ ((π£ β
(TopOpenββfld) β§ π΅ β π£) β ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
33 | 32 | impr 456 |
. . . . . . . 8
β’ ((π£ β
(TopOpenββfld) β§ (π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) β βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) |
34 | 33 | rexlimiva 3141 |
. . . . . . 7
β’
(βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) |
35 | 23, 34 | syl6 35 |
. . . . . 6
β’ (((π β§ πΆ β β) β§ π₯ β β+) β
(βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β βπ¦ β β+ (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
36 | 35 | ralrimdva 3148 |
. . . . 5
β’ ((π β§ πΆ β β) β (βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β βπ₯ β β+ βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
37 | 13 | mopni2 23872 |
. . . . . . . . . 10
β’ (((abs
β β ) β (βMetββ) β§ π’ β (TopOpenββfld)
β§ πΆ β π’) β βπ₯ β β+
(πΆ(ballβ(abs β
β ))π₯) β π’) |
38 | 6, 37 | mp3an1 1449 |
. . . . . . . . 9
β’ ((π’ β
(TopOpenββfld) β§ πΆ β π’) β βπ₯ β β+ (πΆ(ballβ(abs β β
))π₯) β π’) |
39 | | r19.29r 3116 |
. . . . . . . . . . 11
β’
((βπ₯ β
β+ (πΆ(ballβ(abs β β ))π₯) β π’ β§ βπ₯ β β+ βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β βπ₯ β β+
((πΆ(ballβ(abs β
β ))π₯) β π’ β§ βπ¦ β β+ (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
40 | 3 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΆ β β) β§ π₯ β β+) β§ π¦ β β+)
β π΅ β
β) |
41 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΆ β β) β§ π₯ β β+) β§ π¦ β β+)
β π¦ β
β+) |
42 | 41 | rpxrd 12966 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΆ β β) β§ π₯ β β+) β§ π¦ β β+)
β π¦ β
β*) |
43 | 13 | blopn 23879 |
. . . . . . . . . . . . . . . . 17
β’ (((abs
β β ) β (βMetββ) β§ π΅ β β β§ π¦ β β*) β (π΅(ballβ(abs β β
))π¦) β
(TopOpenββfld)) |
44 | 6, 40, 42, 43 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ πΆ β β) β§ π₯ β β+) β§ π¦ β β+)
β (π΅(ballβ(abs
β β ))π¦) β
(TopOpenββfld)) |
45 | | blcntr 23789 |
. . . . . . . . . . . . . . . . 17
β’ (((abs
β β ) β (βMetββ) β§ π΅ β β β§ π¦ β β+) β π΅ β (π΅(ballβ(abs β β ))π¦)) |
46 | 6, 40, 41, 45 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ πΆ β β) β§ π₯ β β+) β§ π¦ β β+)
β π΅ β (π΅(ballβ(abs β β
))π¦)) |
47 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ = (π΅(ballβ(abs β β ))π¦) β (π΅ β π£ β π΅ β (π΅(ballβ(abs β β ))π¦))) |
48 | | ineq1 4169 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π£ = (π΅(ballβ(abs β β ))π¦) β (π£ β© (π΄ β {π΅})) = ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) |
49 | 48 | imaeq2d 6017 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π£ = (π΅(ballβ(abs β β ))π¦) β (πΉ β (π£ β© (π΄ β {π΅}))) = (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅})))) |
50 | 49 | sseq1d 3979 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ = (π΅(ballβ(abs β β ))π¦) β ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
51 | 47, 50 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = (π΅(ballβ(abs β β ))π¦) β ((π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β (π΅ β (π΅(ballβ(abs β β ))π¦) β§ (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)))) |
52 | 51 | rspcev 3583 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅(ballβ(abs β β
))π¦) β
(TopOpenββfld) β§ (π΅ β (π΅(ballβ(abs β β ))π¦) β§ (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
53 | 52 | expr 458 |
. . . . . . . . . . . . . . . 16
β’ (((π΅(ballβ(abs β β
))π¦) β
(TopOpenββfld) β§ π΅ β (π΅(ballβ(abs β β ))π¦)) β ((πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)))) |
54 | 44, 46, 53 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΆ β β) β§ π₯ β β+) β§ π¦ β β+)
β ((πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)))) |
55 | 54 | rexlimdva 3149 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β) β§ π₯ β β+) β
(βπ¦ β
β+ (πΉ
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)))) |
56 | | sstr2 3955 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β ((πΆ(ballβ(abs β β ))π₯) β π’ β (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ ((πΆ(ballβ(abs β β
))π₯) β π’ β ((πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) |
58 | 57 | anim2d 613 |
. . . . . . . . . . . . . . 15
β’ ((πΆ(ballβ(abs β β
))π₯) β π’ β ((π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β (π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’))) |
59 | 58 | reximdv 3164 |
. . . . . . . . . . . . . 14
β’ ((πΆ(ballβ(abs β β
))π₯) β π’ β (βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’))) |
60 | 55, 59 | syl9 77 |
. . . . . . . . . . . . 13
β’ (((π β§ πΆ β β) β§ π₯ β β+) β ((πΆ(ballβ(abs β β
))π₯) β π’ β (βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)))) |
61 | 60 | impd 412 |
. . . . . . . . . . . 12
β’ (((π β§ πΆ β β) β§ π₯ β β+) β (((πΆ(ballβ(abs β β
))π₯) β π’ β§ βπ¦ β β+ (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’))) |
62 | 61 | rexlimdva 3149 |
. . . . . . . . . . 11
β’ ((π β§ πΆ β β) β (βπ₯ β β+
((πΆ(ballβ(abs β
β ))π₯) β π’ β§ βπ¦ β β+ (πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’))) |
63 | 39, 62 | syl5 34 |
. . . . . . . . . 10
β’ ((π β§ πΆ β β) β ((βπ₯ β β+
(πΆ(ballβ(abs β
β ))π₯) β π’ β§ βπ₯ β β+
βπ¦ β
β+ (πΉ
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯)) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’))) |
64 | 63 | expd 417 |
. . . . . . . . 9
β’ ((π β§ πΆ β β) β (βπ₯ β β+
(πΆ(ballβ(abs β
β ))π₯) β π’ β (βπ₯ β β+
βπ¦ β
β+ (πΉ
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)))) |
65 | 38, 64 | syl5 34 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β ((π’ β (TopOpenββfld)
β§ πΆ β π’) β (βπ₯ β β+
βπ¦ β
β+ (πΉ
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)))) |
66 | 65 | expdimp 454 |
. . . . . . 7
β’ (((π β§ πΆ β β) β§ π’ β
(TopOpenββfld)) β (πΆ β π’ β (βπ₯ β β+ βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)))) |
67 | 66 | com23 86 |
. . . . . 6
β’ (((π β§ πΆ β β) β§ π’ β
(TopOpenββfld)) β (βπ₯ β β+ βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β (πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)))) |
68 | 67 | ralrimdva 3148 |
. . . . 5
β’ ((π β§ πΆ β β) β (βπ₯ β β+
βπ¦ β
β+ (πΉ
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)))) |
69 | 36, 68 | impbid 211 |
. . . 4
β’ ((π β§ πΆ β β) β (βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β βπ₯ β β+ βπ¦ β β+
(πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯))) |
70 | 1 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β πΉ:π΄βΆβ) |
71 | 70 | ffund 6676 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β Fun πΉ) |
72 | | inss2 4193 |
. . . . . . . . . 10
β’ ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅})) β (π΄ β {π΅}) |
73 | | difss 4095 |
. . . . . . . . . . 11
β’ (π΄ β {π΅}) β π΄ |
74 | 70 | fdmd 6683 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β dom πΉ = π΄) |
75 | 73, 74 | sseqtrrid 4001 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β (π΄ β {π΅}) β dom πΉ) |
76 | 72, 75 | sstrid 3959 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅})) β dom πΉ) |
77 | | funimass4 6911 |
. . . . . . . . 9
β’ ((Fun
πΉ β§ ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅})) β dom πΉ) β ((πΉ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ§ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))(πΉβπ§) β (πΆ(ballβ(abs β β ))π₯))) |
78 | 71, 76, 77 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β ((πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ§ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))(πΉβπ§) β (πΆ(ballβ(abs β β ))π₯))) |
79 | 6 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β (abs β β ) β
(βMetββ)) |
80 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β π¦ β β+) |
81 | 80 | rpxrd 12966 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β π¦ β β*) |
82 | 3 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β π΅ β β) |
83 | 73, 2 | sstrid 3959 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ β {π΅}) β β) |
84 | 83 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β (π΄ β {π΅}) β
β) |
85 | 84 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β π§ β β) |
86 | | elbl3 23768 |
. . . . . . . . . . . . 13
β’ ((((abs
β β ) β (βMetββ) β§ π¦ β β*) β§ (π΅ β β β§ π§ β β)) β (π§ β (π΅(ballβ(abs β β ))π¦) β (π§(abs β β )π΅) < π¦)) |
87 | 79, 81, 82, 85, 86 | syl22anc 838 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β (π§ β (π΅(ballβ(abs β β ))π¦) β (π§(abs β β )π΅) < π¦)) |
88 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (abs
β β ) = (abs β β ) |
89 | 88 | cnmetdval 24157 |
. . . . . . . . . . . . . 14
β’ ((π§ β β β§ π΅ β β) β (π§(abs β β )π΅) = (absβ(π§ β π΅))) |
90 | 85, 82, 89 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β (π§(abs β β )π΅) = (absβ(π§ β π΅))) |
91 | 90 | breq1d 5119 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β ((π§(abs β β )π΅) < π¦ β (absβ(π§ β π΅)) < π¦)) |
92 | 87, 91 | bitrd 279 |
. . . . . . . . . . 11
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β (π§ β (π΅(ballβ(abs β β ))π¦) β (absβ(π§ β π΅)) < π¦)) |
93 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β π₯ β β+) |
94 | 93 | rpxrd 12966 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β π₯ β β*) |
95 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β πΆ β β) |
96 | | eldifi 4090 |
. . . . . . . . . . . . . 14
β’ (π§ β (π΄ β {π΅}) β π§ β π΄) |
97 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((πΉ:π΄βΆβ β§ π§ β π΄) β (πΉβπ§) β β) |
98 | 70, 96, 97 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β (πΉβπ§) β β) |
99 | | elbl3 23768 |
. . . . . . . . . . . . 13
β’ ((((abs
β β ) β (βMetββ) β§ π₯ β β*) β§ (πΆ β β β§ (πΉβπ§) β β)) β ((πΉβπ§) β (πΆ(ballβ(abs β β ))π₯) β ((πΉβπ§)(abs β β )πΆ) < π₯)) |
100 | 79, 94, 95, 98, 99 | syl22anc 838 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β ((πΉβπ§) β (πΆ(ballβ(abs β β ))π₯) β ((πΉβπ§)(abs β β )πΆ) < π₯)) |
101 | 88 | cnmetdval 24157 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ§) β β β§ πΆ β β) β ((πΉβπ§)(abs β β )πΆ) = (absβ((πΉβπ§) β πΆ))) |
102 | 98, 95, 101 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β ((πΉβπ§)(abs β β )πΆ) = (absβ((πΉβπ§) β πΆ))) |
103 | 102 | breq1d 5119 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β (((πΉβπ§)(abs β β )πΆ) < π₯ β (absβ((πΉβπ§) β πΆ)) < π₯)) |
104 | 100, 103 | bitrd 279 |
. . . . . . . . . . 11
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β ((πΉβπ§) β (πΆ(ballβ(abs β β ))π₯) β (absβ((πΉβπ§) β πΆ)) < π₯)) |
105 | 92, 104 | imbi12d 345 |
. . . . . . . . . 10
β’ ((((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β§ π§ β (π΄ β {π΅})) β ((π§ β (π΅(ballβ(abs β β ))π¦) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯)) β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯))) |
106 | 105 | ralbidva 3169 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β (βπ§ β
(π΄ β {π΅})(π§ β (π΅(ballβ(abs β β ))π¦) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯)) β βπ§ β (π΄ β {π΅})((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯))) |
107 | | elin 3930 |
. . . . . . . . . . . . 13
β’ (π§ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅})) β (π§ β (π΅(ballβ(abs β β ))π¦) β§ π§ β (π΄ β {π΅}))) |
108 | 107 | biancomi 464 |
. . . . . . . . . . . 12
β’ (π§ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅})) β (π§ β (π΄ β {π΅}) β§ π§ β (π΅(ballβ(abs β β ))π¦))) |
109 | 108 | imbi1i 350 |
. . . . . . . . . . 11
β’ ((π§ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅})) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯)) β ((π§ β (π΄ β {π΅}) β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯))) |
110 | | impexp 452 |
. . . . . . . . . . 11
β’ (((π§ β (π΄ β {π΅}) β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯)) β (π§ β (π΄ β {π΅}) β (π§ β (π΅(ballβ(abs β β ))π¦) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯)))) |
111 | 109, 110 | bitr2i 276 |
. . . . . . . . . 10
β’ ((π§ β (π΄ β {π΅}) β (π§ β (π΅(ballβ(abs β β ))π¦) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯))) β (π§ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅})) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯))) |
112 | 111 | ralbii2 3089 |
. . . . . . . . 9
β’
(βπ§ β
(π΄ β {π΅})(π§ β (π΅(ballβ(abs β β ))π¦) β (πΉβπ§) β (πΆ(ballβ(abs β β ))π₯)) β βπ§ β ((π΅(ballβ(abs β β ))π¦) β© (π΄ β {π΅}))(πΉβπ§) β (πΆ(ballβ(abs β β ))π₯)) |
113 | | impexp 452 |
. . . . . . . . . . 11
β’ (((π§ β π΄ β§ π§ β π΅) β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯)) β (π§ β π΄ β (π§ β π΅ β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯)))) |
114 | | eldifsn 4751 |
. . . . . . . . . . . 12
β’ (π§ β (π΄ β {π΅}) β (π§ β π΄ β§ π§ β π΅)) |
115 | 114 | imbi1i 350 |
. . . . . . . . . . 11
β’ ((π§ β (π΄ β {π΅}) β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯)) β ((π§ β π΄ β§ π§ β π΅) β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯))) |
116 | | impexp 452 |
. . . . . . . . . . . 12
β’ (((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯) β (π§ β π΅ β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯))) |
117 | 116 | imbi2i 336 |
. . . . . . . . . . 11
β’ ((π§ β π΄ β ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯)) β (π§ β π΄ β (π§ β π΅ β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯)))) |
118 | 113, 115,
117 | 3bitr4i 303 |
. . . . . . . . . 10
β’ ((π§ β (π΄ β {π΅}) β ((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯)) β (π§ β π΄ β ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯))) |
119 | 118 | ralbii2 3089 |
. . . . . . . . 9
β’
(βπ§ β
(π΄ β {π΅})((absβ(π§ β π΅)) < π¦ β (absβ((πΉβπ§) β πΆ)) < π₯) β βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯)) |
120 | 106, 112,
119 | 3bitr3g 313 |
. . . . . . . 8
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β (βπ§ β
((π΅(ballβ(abs β
β ))π¦) β© (π΄ β {π΅}))(πΉβπ§) β (πΆ(ballβ(abs β β ))π₯) β βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯))) |
121 | 78, 120 | bitrd 279 |
. . . . . . 7
β’ (((π β§ πΆ β β) β§ (π₯ β β+ β§ π¦ β β+))
β ((πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯))) |
122 | 121 | anassrs 469 |
. . . . . 6
β’ ((((π β§ πΆ β β) β§ π₯ β β+) β§ π¦ β β+)
β ((πΉ β ((π΅(ballβ(abs β β
))π¦) β© (π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯))) |
123 | 122 | rexbidva 3170 |
. . . . 5
β’ (((π β§ πΆ β β) β§ π₯ β β+) β
(βπ¦ β
β+ (πΉ
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ¦ β β+
βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯))) |
124 | 123 | ralbidva 3169 |
. . . 4
β’ ((π β§ πΆ β β) β (βπ₯ β β+
βπ¦ β
β+ (πΉ
β ((π΅(ballβ(abs
β β ))π¦) β©
(π΄ β {π΅}))) β (πΆ(ballβ(abs β β ))π₯) β βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯))) |
125 | 69, 124 | bitrd 279 |
. . 3
β’ ((π β§ πΆ β β) β (βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’)) β βπ₯ β β+ βπ¦ β β+
βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯))) |
126 | 125 | pm5.32da 580 |
. 2
β’ (π β ((πΆ β β β§ βπ’ β
(TopOpenββfld)(πΆ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (π΄ β {π΅}))) β π’))) β (πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯)))) |
127 | 5, 126 | bitrd 279 |
1
β’ (π β (πΆ β (πΉ limβ π΅) β (πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯)))) |