Step | Hyp | Ref
| Expression |
1 | | inss1 4193 |
. . . . . . . . . 10
β’ (π’ β© π) β π’ |
2 | | metrest.3 |
. . . . . . . . . . . . 13
β’ π½ = (MetOpenβπΆ) |
3 | 2 | elmopn2 23814 |
. . . . . . . . . . . 12
β’ (πΆ β (βMetβπ) β (π’ β π½ β (π’ β π β§ βπ¦ β π’ βπ β β+ (π¦(ballβπΆ)π) β π’))) |
4 | 3 | simplbda 501 |
. . . . . . . . . . 11
β’ ((πΆ β (βMetβπ) β§ π’ β π½) β βπ¦ β π’ βπ β β+ (π¦(ballβπΆ)π) β π’) |
5 | 4 | adantlr 714 |
. . . . . . . . . 10
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π’ β π½) β βπ¦ β π’ βπ β β+ (π¦(ballβπΆ)π) β π’) |
6 | | ssralv 4015 |
. . . . . . . . . 10
β’ ((π’ β© π) β π’ β (βπ¦ β π’ βπ β β+ (π¦(ballβπΆ)π) β π’ β βπ¦ β (π’ β© π)βπ β β+ (π¦(ballβπΆ)π) β π’)) |
7 | 1, 5, 6 | mpsyl 68 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π’ β π½) β βπ¦ β (π’ β© π)βπ β β+ (π¦(ballβπΆ)π) β π’) |
8 | | ssrin 4198 |
. . . . . . . . . . 11
β’ ((π¦(ballβπΆ)π) β π’ β ((π¦(ballβπΆ)π) β© π) β (π’ β© π)) |
9 | 8 | reximi 3088 |
. . . . . . . . . 10
β’
(βπ β
β+ (π¦(ballβπΆ)π) β π’ β βπ β β+ ((π¦(ballβπΆ)π) β© π) β (π’ β© π)) |
10 | 9 | ralimi 3087 |
. . . . . . . . 9
β’
(βπ¦ β
(π’ β© π)βπ β β+ (π¦(ballβπΆ)π) β π’ β βπ¦ β (π’ β© π)βπ β β+ ((π¦(ballβπΆ)π) β© π) β (π’ β© π)) |
11 | 7, 10 | syl 17 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π’ β π½) β βπ¦ β (π’ β© π)βπ β β+ ((π¦(ballβπΆ)π) β© π) β (π’ β© π)) |
12 | | inss2 4194 |
. . . . . . . 8
β’ (π’ β© π) β π |
13 | 11, 12 | jctil 521 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π’ β π½) β ((π’ β© π) β π β§ βπ¦ β (π’ β© π)βπ β β+ ((π¦(ballβπΆ)π) β© π) β (π’ β© π))) |
14 | | sseq1 3974 |
. . . . . . . 8
β’ (π₯ = (π’ β© π) β (π₯ β π β (π’ β© π) β π)) |
15 | | sseq2 3975 |
. . . . . . . . . 10
β’ (π₯ = (π’ β© π) β (((π¦(ballβπΆ)π) β© π) β π₯ β ((π¦(ballβπΆ)π) β© π) β (π’ β© π))) |
16 | 15 | rexbidv 3176 |
. . . . . . . . 9
β’ (π₯ = (π’ β© π) β (βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯ β βπ β β+ ((π¦(ballβπΆ)π) β© π) β (π’ β© π))) |
17 | 16 | raleqbi1dv 3310 |
. . . . . . . 8
β’ (π₯ = (π’ β© π) β (βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯ β βπ¦ β (π’ β© π)βπ β β+ ((π¦(ballβπΆ)π) β© π) β (π’ β© π))) |
18 | 14, 17 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = (π’ β© π) β ((π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯) β ((π’ β© π) β π β§ βπ¦ β (π’ β© π)βπ β β+ ((π¦(ballβπΆ)π) β© π) β (π’ β© π)))) |
19 | 13, 18 | syl5ibrcom 247 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π’ β π½) β (π₯ = (π’ β© π) β (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯))) |
20 | 19 | rexlimdva 3153 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π β π) β (βπ’ β π½ π₯ = (π’ β© π) β (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯))) |
21 | 2 | mopntop 23809 |
. . . . . . . . 9
β’ (πΆ β (βMetβπ) β π½ β Top) |
22 | 21 | ad2antrr 725 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β π½ β Top) |
23 | | ssel2 3944 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π β§ π¦ β π₯) β π¦ β π) |
24 | | ssel2 3944 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π¦ β π) β π¦ β π) |
25 | | rpxr 12931 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β+
β π β
β*) |
26 | 2 | blopn 23872 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΆ β (βMetβπ) β§ π¦ β π β§ π β β*) β (π¦(ballβπΆ)π) β π½) |
27 | | eleq1a 2833 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦(ballβπΆ)π) β π½ β (π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΆ β (βMetβπ) β§ π¦ β π β§ π β β*) β (π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
29 | 28 | 3expa 1119 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΆ β (βMetβπ) β§ π¦ β π) β§ π β β*) β (π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
30 | 25, 29 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ (((πΆ β (βMetβπ) β§ π¦ β π) β§ π β β+) β (π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
31 | 30 | rexlimdva 3153 |
. . . . . . . . . . . . . . . 16
β’ ((πΆ β (βMetβπ) β§ π¦ β π) β (βπ β β+ π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
32 | 24, 31 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((πΆ β (βMetβπ) β§ (π β π β§ π¦ β π)) β (βπ β β+ π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
33 | 32 | anassrs 469 |
. . . . . . . . . . . . . 14
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π¦ β π) β (βπ β β+ π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
34 | 23, 33 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ π¦ β π₯)) β (βπ β β+ π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
35 | 34 | anassrs 469 |
. . . . . . . . . . . 12
β’ ((((πΆ β (βMetβπ) β§ π β π) β§ π₯ β π) β§ π¦ β π₯) β (βπ β β+ π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
36 | 35 | rexlimdva 3153 |
. . . . . . . . . . 11
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π₯ β π) β (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β π§ β π½)) |
37 | 36 | adantrd 493 |
. . . . . . . . . 10
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π₯ β π) β ((βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯) β π§ β π½)) |
38 | 37 | adantrr 716 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β ((βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯) β π§ β π½)) |
39 | 38 | abssdv 4030 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β π½) |
40 | | uniopn 22262 |
. . . . . . . 8
β’ ((π½ β Top β§ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β π½) β βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β π½) |
41 | 22, 39, 40 | syl2anc 585 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β π½) |
42 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π’ β (π¦(ballβπΆ)π) = (π’(ballβπΆ)π)) |
43 | 42 | ineq1d 4176 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π’ β ((π¦(ballβπΆ)π) β© π) = ((π’(ballβπΆ)π) β© π)) |
44 | 43 | sseq1d 3980 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π’ β (((π¦(ballβπΆ)π) β© π) β π₯ β ((π’(ballβπΆ)π) β© π) β π₯)) |
45 | 44 | rexbidv 3176 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π’ β (βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯ β βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯)) |
46 | 45 | rspccv 3581 |
. . . . . . . . . . . . . 14
β’
(βπ¦ β
π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯ β (π’ β π₯ β βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯)) |
47 | 46 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯)) |
48 | | ssel 3942 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π β (π’ β π₯ β π’ β π)) |
49 | | ssel 3942 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (π’ β π β π’ β π)) |
50 | | blcntr 23782 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΆ β (βMetβπ) β§ π’ β π β§ π β β+) β π’ β (π’(ballβπΆ)π)) |
51 | 50 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΆ β (βMetβπ) β§ π’ β π β§ π β β+) β (((π’(ballβπΆ)π) β© π) β π₯ β π’ β (π’(ballβπΆ)π))) |
52 | 51 | ancld 552 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΆ β (βMetβπ) β§ π’ β π β§ π β β+) β (((π’(ballβπΆ)π) β© π) β π₯ β (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π)))) |
53 | 52 | 3expa 1119 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΆ β (βMetβπ) β§ π’ β π) β§ π β β+) β (((π’(ballβπΆ)π) β© π) β π₯ β (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π)))) |
54 | 53 | reximdva 3166 |
. . . . . . . . . . . . . . . . 17
β’ ((πΆ β (βMetβπ) β§ π’ β π) β (βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯ β βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π)))) |
55 | 54 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (πΆ β (βMetβπ) β (π’ β π β (βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯ β βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π))))) |
56 | 49, 55 | sylan9r 510 |
. . . . . . . . . . . . . . 15
β’ ((πΆ β (βMetβπ) β§ π β π) β (π’ β π β (βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯ β βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π))))) |
57 | 48, 56 | sylan9r 510 |
. . . . . . . . . . . . . 14
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π₯ β π) β (π’ β π₯ β (βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯ β βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π))))) |
58 | 57 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β (βπ β β+ ((π’(ballβπΆ)π) β© π) β π₯ β βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π))))) |
59 | 47, 58 | mpdd 43 |
. . . . . . . . . . . 12
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π)))) |
60 | 42 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π’ β (π’ β (π¦(ballβπΆ)π) β π’ β (π’(ballβπΆ)π))) |
61 | 44, 60 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π’ β ((((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π)))) |
62 | 61 | rexbidv 3176 |
. . . . . . . . . . . . . 14
β’ (π¦ = π’ β (βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π)))) |
63 | 62 | rspcev 3584 |
. . . . . . . . . . . . 13
β’ ((π’ β π₯ β§ βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π))) β βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π))) |
64 | 63 | ex 414 |
. . . . . . . . . . . 12
β’ (π’ β π₯ β (βπ β β+ (((π’(ballβπΆ)π) β© π) β π₯ β§ π’ β (π’(ballβπΆ)π)) β βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)))) |
65 | 59, 64 | sylcom 30 |
. . . . . . . . . . 11
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)))) |
66 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β π₯ β π) |
67 | 66 | sseld 3948 |
. . . . . . . . . . 11
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β π’ β π)) |
68 | 65, 67 | jcad 514 |
. . . . . . . . . 10
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β (βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β§ π’ β π))) |
69 | | elin 3931 |
. . . . . . . . . . . . . . 15
β’ (π’ β ((π¦(ballβπΆ)π) β© π) β (π’ β (π¦(ballβπΆ)π) β§ π’ β π)) |
70 | | ssel2 3944 |
. . . . . . . . . . . . . . 15
β’ ((((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β ((π¦(ballβπΆ)π) β© π)) β π’ β π₯) |
71 | 69, 70 | sylan2br 596 |
. . . . . . . . . . . . . 14
β’ ((((π¦(ballβπΆ)π) β© π) β π₯ β§ (π’ β (π¦(ballβπΆ)π) β§ π’ β π)) β π’ β π₯) |
72 | 71 | expr 458 |
. . . . . . . . . . . . 13
β’ ((((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β (π’ β π β π’ β π₯)) |
73 | 72 | rexlimivw 3149 |
. . . . . . . . . . . 12
β’
(βπ β
β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β (π’ β π β π’ β π₯)) |
74 | 73 | rexlimivw 3149 |
. . . . . . . . . . 11
β’
(βπ¦ β
π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β (π’ β π β π’ β π₯)) |
75 | 74 | imp 408 |
. . . . . . . . . 10
β’
((βπ¦ β
π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β§ π’ β π) β π’ β π₯) |
76 | 68, 75 | impbid1 224 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β (βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β§ π’ β π))) |
77 | | elin 3931 |
. . . . . . . . . 10
β’ (π’ β (βͺ {π§
β£ (βπ¦ β
π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β© π) β (π’ β βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β§ π’ β π)) |
78 | | eluniab 4885 |
. . . . . . . . . . . 12
β’ (π’ β βͺ {π§
β£ (βπ¦ β
π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β βπ§(π’ β π§ β§ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯))) |
79 | | ancom 462 |
. . . . . . . . . . . . . 14
β’ ((π’ β π§ β§ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)) β ((βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯) β§ π’ β π§)) |
80 | | anass 470 |
. . . . . . . . . . . . . 14
β’
(((βπ¦ β
π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯) β§ π’ β π§) β (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
81 | | r19.41v 3186 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
β+ (π§ =
(π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β (βπ β β+ π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
82 | 81 | rexbii 3098 |
. . . . . . . . . . . . . . 15
β’
(βπ¦ β
π₯ βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β βπ¦ β π₯ (βπ β β+ π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
83 | | r19.41v 3186 |
. . . . . . . . . . . . . . 15
β’
(βπ¦ β
π₯ (βπ β β+
π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
84 | 82, 83 | bitr2i 276 |
. . . . . . . . . . . . . 14
β’
((βπ¦ β
π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β βπ¦ β π₯ βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
85 | 79, 80, 84 | 3bitri 297 |
. . . . . . . . . . . . 13
β’ ((π’ β π§ β§ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)) β βπ¦ β π₯ βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
86 | 85 | exbii 1851 |
. . . . . . . . . . . 12
β’
(βπ§(π’ β π§ β§ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)) β βπ§βπ¦ β π₯ βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
87 | | ovex 7395 |
. . . . . . . . . . . . . . . . 17
β’ (π¦(ballβπΆ)π) β V |
88 | | ineq1 4170 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (π¦(ballβπΆ)π) β (π§ β© π) = ((π¦(ballβπΆ)π) β© π)) |
89 | 88 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (π¦(ballβπΆ)π) β ((π§ β© π) β π₯ β ((π¦(ballβπΆ)π) β© π) β π₯)) |
90 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (π¦(ballβπΆ)π) β (π’ β π§ β π’ β (π¦(ballβπΆ)π))) |
91 | 89, 90 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π¦(ballβπΆ)π) β (((π§ β© π) β π₯ β§ π’ β π§) β (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)))) |
92 | 87, 91 | ceqsexv 3497 |
. . . . . . . . . . . . . . . 16
β’
(βπ§(π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π))) |
93 | 92 | rexbii 3098 |
. . . . . . . . . . . . . . 15
β’
(βπ β
β+ βπ§(π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π))) |
94 | | rexcom4 3274 |
. . . . . . . . . . . . . . 15
β’
(βπ β
β+ βπ§(π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β βπ§βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
95 | 93, 94 | bitr3i 277 |
. . . . . . . . . . . . . 14
β’
(βπ β
β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β βπ§βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
96 | 95 | rexbii 3098 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β βπ¦ β π₯ βπ§βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
97 | | rexcom4 3274 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
π₯ βπ§βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β βπ§βπ¦ β π₯ βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§))) |
98 | 96, 97 | bitr2i 276 |
. . . . . . . . . . . 12
β’
(βπ§βπ¦ β π₯ βπ β β+ (π§ = (π¦(ballβπΆ)π) β§ ((π§ β© π) β π₯ β§ π’ β π§)) β βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π))) |
99 | 78, 86, 98 | 3bitri 297 |
. . . . . . . . . . 11
β’ (π’ β βͺ {π§
β£ (βπ¦ β
π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π))) |
100 | 99 | anbi1i 625 |
. . . . . . . . . 10
β’ ((π’ β βͺ {π§
β£ (βπ¦ β
π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β§ π’ β π) β (βπ¦ β π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β§ π’ β π)) |
101 | 77, 100 | bitr2i 276 |
. . . . . . . . 9
β’
((βπ¦ β
π₯ βπ β β+ (((π¦(ballβπΆ)π) β© π) β π₯ β§ π’ β (π¦(ballβπΆ)π)) β§ π’ β π) β π’ β (βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β© π)) |
102 | 76, 101 | bitrdi 287 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β (π’ β π₯ β π’ β (βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β© π))) |
103 | 102 | eqrdv 2735 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β π₯ = (βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β© π)) |
104 | | ineq1 4170 |
. . . . . . . 8
β’ (π’ = βͺ
{π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β (π’ β© π) = (βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β© π)) |
105 | 104 | rspceeqv 3600 |
. . . . . . 7
β’ ((βͺ {π§
β£ (βπ¦ β
π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β π½ β§ π₯ = (βͺ {π§ β£ (βπ¦ β π₯ βπ β β+ π§ = (π¦(ballβπΆ)π) β§ (π§ β© π) β π₯)} β© π)) β βπ’ β π½ π₯ = (π’ β© π)) |
106 | 41, 103, 105 | syl2anc 585 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) β βπ’ β π½ π₯ = (π’ β© π)) |
107 | 106 | ex 414 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π β π) β ((π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯) β βπ’ β π½ π₯ = (π’ β© π))) |
108 | 20, 107 | impbid 211 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π β π) β (βπ’ β π½ π₯ = (π’ β© π) β (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯))) |
109 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β π β§ π¦ β π) β π¦ β π) |
110 | 24, 109 | elind 4159 |
. . . . . . . . . 10
β’ ((π β π β§ π¦ β π) β π¦ β (π β© π)) |
111 | | metrest.1 |
. . . . . . . . . . . . . . 15
β’ π· = (πΆ βΎ (π Γ π)) |
112 | 111 | blres 23800 |
. . . . . . . . . . . . . 14
β’ ((πΆ β (βMetβπ) β§ π¦ β (π β© π) β§ π β β*) β (π¦(ballβπ·)π) = ((π¦(ballβπΆ)π) β© π)) |
113 | 112 | sseq1d 3980 |
. . . . . . . . . . . . 13
β’ ((πΆ β (βMetβπ) β§ π¦ β (π β© π) β§ π β β*) β ((π¦(ballβπ·)π) β π₯ β ((π¦(ballβπΆ)π) β© π) β π₯)) |
114 | 113 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((πΆ β (βMetβπ) β§ π¦ β (π β© π)) β§ π β β*) β ((π¦(ballβπ·)π) β π₯ β ((π¦(ballβπΆ)π) β© π) β π₯)) |
115 | 25, 114 | sylan2 594 |
. . . . . . . . . . 11
β’ (((πΆ β (βMetβπ) β§ π¦ β (π β© π)) β§ π β β+) β ((π¦(ballβπ·)π) β π₯ β ((π¦(ballβπΆ)π) β© π) β π₯)) |
116 | 115 | rexbidva 3174 |
. . . . . . . . . 10
β’ ((πΆ β (βMetβπ) β§ π¦ β (π β© π)) β (βπ β β+ (π¦(ballβπ·)π) β π₯ β βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) |
117 | 110, 116 | sylan2 594 |
. . . . . . . . 9
β’ ((πΆ β (βMetβπ) β§ (π β π β§ π¦ β π)) β (βπ β β+ (π¦(ballβπ·)π) β π₯ β βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) |
118 | 117 | anassrs 469 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π¦ β π) β (βπ β β+ (π¦(ballβπ·)π) β π₯ β βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) |
119 | 23, 118 | sylan2 594 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π β π) β§ (π₯ β π β§ π¦ β π₯)) β (βπ β β+ (π¦(ballβπ·)π) β π₯ β βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) |
120 | 119 | anassrs 469 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π β π) β§ π₯ β π) β§ π¦ β π₯) β (βπ β β+ (π¦(ballβπ·)π) β π₯ β βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) |
121 | 120 | ralbidva 3173 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π β π) β§ π₯ β π) β (βπ¦ β π₯ βπ β β+ (π¦(ballβπ·)π) β π₯ β βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯)) |
122 | 121 | pm5.32da 580 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π β π) β ((π₯ β π β§ βπ¦ β π₯ βπ β β+ (π¦(ballβπ·)π) β π₯) β (π₯ β π β§ βπ¦ β π₯ βπ β β+ ((π¦(ballβπΆ)π) β© π) β π₯))) |
123 | 108, 122 | bitr4d 282 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π β π) β (βπ’ β π½ π₯ = (π’ β© π) β (π₯ β π β§ βπ¦ β π₯ βπ β β+ (π¦(ballβπ·)π) β π₯))) |
124 | | id 22 |
. . . . 5
β’ (π β π β π β π) |
125 | 2 | mopnm 23813 |
. . . . 5
β’ (πΆ β (βMetβπ) β π β π½) |
126 | | ssexg 5285 |
. . . . 5
β’ ((π β π β§ π β π½) β π β V) |
127 | 124, 125,
126 | syl2anr 598 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π β π) β π β V) |
128 | | elrest 17316 |
. . . 4
β’ ((π½ β Top β§ π β V) β (π₯ β (π½ βΎt π) β βπ’ β π½ π₯ = (π’ β© π))) |
129 | 21, 127, 128 | syl2an2r 684 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π β π) β (π₯ β (π½ βΎt π) β βπ’ β π½ π₯ = (π’ β© π))) |
130 | | xmetres2 23730 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π β π) β (πΆ βΎ (π Γ π)) β (βMetβπ)) |
131 | 111, 130 | eqeltrid 2842 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π β π) β π· β (βMetβπ)) |
132 | | metrest.4 |
. . . . 5
β’ πΎ = (MetOpenβπ·) |
133 | 132 | elmopn2 23814 |
. . . 4
β’ (π· β (βMetβπ) β (π₯ β πΎ β (π₯ β π β§ βπ¦ β π₯ βπ β β+ (π¦(ballβπ·)π) β π₯))) |
134 | 131, 133 | syl 17 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π β π) β (π₯ β πΎ β (π₯ β π β§ βπ¦ β π₯ βπ β β+ (π¦(ballβπ·)π) β π₯))) |
135 | 123, 129,
134 | 3bitr4d 311 |
. 2
β’ ((πΆ β (βMetβπ) β§ π β π) β (π₯ β (π½ βΎt π) β π₯ β πΎ)) |
136 | 135 | eqrdv 2735 |
1
β’ ((πΆ β (βMetβπ) β§ π β π) β (π½ βΎt π) = πΎ) |