Step | Hyp | Ref
| Expression |
1 | | methaus.1 |
. . 3
β’ π½ = (MetOpenβπ·) |
2 | 1 | mopnex 23891 |
. 2
β’ (π· β (βMetβπ) β βπ β (Metβπ)π½ = (MetOpenβπ)) |
3 | | metxmet 23703 |
. . . . . . . . . 10
β’ (π β (Metβπ) β π β (βMetβπ)) |
4 | 3 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β π β (βMetβπ)) |
5 | | simplrl 776 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β π₯ β π) |
6 | | metcl 23701 |
. . . . . . . . . . . . . 14
β’ ((π β (Metβπ) β§ π₯ β π β§ π¦ β π) β (π₯ππ¦) β β) |
7 | 6 | 3expb 1121 |
. . . . . . . . . . . . 13
β’ ((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β β) |
8 | 7 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (π₯ππ¦) β β) |
9 | | metgt0 23728 |
. . . . . . . . . . . . . 14
β’ ((π β (Metβπ) β§ π₯ β π β§ π¦ β π) β (π₯ β π¦ β 0 < (π₯ππ¦))) |
10 | 9 | 3expb 1121 |
. . . . . . . . . . . . 13
β’ ((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯ β π¦ β 0 < (π₯ππ¦))) |
11 | 10 | biimpa 478 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β 0 < (π₯ππ¦)) |
12 | 8, 11 | elrpd 12961 |
. . . . . . . . . . 11
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (π₯ππ¦) β
β+) |
13 | 12 | rphalfcld 12976 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β ((π₯ππ¦) / 2) β
β+) |
14 | 13 | rpxrd 12965 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β ((π₯ππ¦) / 2) β
β*) |
15 | | eqid 2737 |
. . . . . . . . . 10
β’
(MetOpenβπ) =
(MetOpenβπ) |
16 | 15 | blopn 23872 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ π₯ β π β§ ((π₯ππ¦) / 2) β β*) β
(π₯(ballβπ)((π₯ππ¦) / 2)) β (MetOpenβπ)) |
17 | 4, 5, 14, 16 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (π₯(ballβπ)((π₯ππ¦) / 2)) β (MetOpenβπ)) |
18 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β π¦ β π) |
19 | 15 | blopn 23872 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ π¦ β π β§ ((π₯ππ¦) / 2) β β*) β
(π¦(ballβπ)((π₯ππ¦) / 2)) β (MetOpenβπ)) |
20 | 4, 18, 14, 19 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (π¦(ballβπ)((π₯ππ¦) / 2)) β (MetOpenβπ)) |
21 | | blcntr 23782 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ π₯ β π β§ ((π₯ππ¦) / 2) β β+) β
π₯ β (π₯(ballβπ)((π₯ππ¦) / 2))) |
22 | 4, 5, 13, 21 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β π₯ β (π₯(ballβπ)((π₯ππ¦) / 2))) |
23 | | blcntr 23782 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ π¦ β π β§ ((π₯ππ¦) / 2) β β+) β
π¦ β (π¦(ballβπ)((π₯ππ¦) / 2))) |
24 | 4, 18, 13, 23 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β π¦ β (π¦(ballβπ)((π₯ππ¦) / 2))) |
25 | 13 | rpred 12964 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β ((π₯ππ¦) / 2) β β) |
26 | 25, 25 | rexaddd 13160 |
. . . . . . . . . . 11
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (((π₯ππ¦) / 2) +π ((π₯ππ¦) / 2)) = (((π₯ππ¦) / 2) + ((π₯ππ¦) / 2))) |
27 | 8 | recnd 11190 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (π₯ππ¦) β β) |
28 | 27 | 2halvesd 12406 |
. . . . . . . . . . 11
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (((π₯ππ¦) / 2) + ((π₯ππ¦) / 2)) = (π₯ππ¦)) |
29 | 26, 28 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (((π₯ππ¦) / 2) +π ((π₯ππ¦) / 2)) = (π₯ππ¦)) |
30 | 8 | leidd 11728 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (π₯ππ¦) β€ (π₯ππ¦)) |
31 | 29, 30 | eqbrtrd 5132 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β (((π₯ππ¦) / 2) +π ((π₯ππ¦) / 2)) β€ (π₯ππ¦)) |
32 | | bldisj 23767 |
. . . . . . . . 9
β’ (((π β (βMetβπ) β§ π₯ β π β§ π¦ β π) β§ (((π₯ππ¦) / 2) β β* β§
((π₯ππ¦) / 2) β β* β§
(((π₯ππ¦) / 2) +π ((π₯ππ¦) / 2)) β€ (π₯ππ¦))) β ((π₯(ballβπ)((π₯ππ¦) / 2)) β© (π¦(ballβπ)((π₯ππ¦) / 2))) = β
) |
33 | 4, 5, 18, 14, 14, 31, 32 | syl33anc 1386 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β ((π₯(ballβπ)((π₯ππ¦) / 2)) β© (π¦(ballβπ)((π₯ππ¦) / 2))) = β
) |
34 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π = (π₯(ballβπ)((π₯ππ¦) / 2)) β (π₯ β π β π₯ β (π₯(ballβπ)((π₯ππ¦) / 2)))) |
35 | | ineq1 4170 |
. . . . . . . . . . 11
β’ (π = (π₯(ballβπ)((π₯ππ¦) / 2)) β (π β© π) = ((π₯(ballβπ)((π₯ππ¦) / 2)) β© π)) |
36 | 35 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π = (π₯(ballβπ)((π₯ππ¦) / 2)) β ((π β© π) = β
β ((π₯(ballβπ)((π₯ππ¦) / 2)) β© π) = β
)) |
37 | 34, 36 | 3anbi13d 1439 |
. . . . . . . . 9
β’ (π = (π₯(ballβπ)((π₯ππ¦) / 2)) β ((π₯ β π β§ π¦ β π β§ (π β© π) = β
) β (π₯ β (π₯(ballβπ)((π₯ππ¦) / 2)) β§ π¦ β π β§ ((π₯(ballβπ)((π₯ππ¦) / 2)) β© π) = β
))) |
38 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π = (π¦(ballβπ)((π₯ππ¦) / 2)) β (π¦ β π β π¦ β (π¦(ballβπ)((π₯ππ¦) / 2)))) |
39 | | ineq2 4171 |
. . . . . . . . . . 11
β’ (π = (π¦(ballβπ)((π₯ππ¦) / 2)) β ((π₯(ballβπ)((π₯ππ¦) / 2)) β© π) = ((π₯(ballβπ)((π₯ππ¦) / 2)) β© (π¦(ballβπ)((π₯ππ¦) / 2)))) |
40 | 39 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π = (π¦(ballβπ)((π₯ππ¦) / 2)) β (((π₯(ballβπ)((π₯ππ¦) / 2)) β© π) = β
β ((π₯(ballβπ)((π₯ππ¦) / 2)) β© (π¦(ballβπ)((π₯ππ¦) / 2))) = β
)) |
41 | 38, 40 | 3anbi23d 1440 |
. . . . . . . . 9
β’ (π = (π¦(ballβπ)((π₯ππ¦) / 2)) β ((π₯ β (π₯(ballβπ)((π₯ππ¦) / 2)) β§ π¦ β π β§ ((π₯(ballβπ)((π₯ππ¦) / 2)) β© π) = β
) β (π₯ β (π₯(ballβπ)((π₯ππ¦) / 2)) β§ π¦ β (π¦(ballβπ)((π₯ππ¦) / 2)) β§ ((π₯(ballβπ)((π₯ππ¦) / 2)) β© (π¦(ballβπ)((π₯ππ¦) / 2))) = β
))) |
42 | 37, 41 | rspc2ev 3595 |
. . . . . . . 8
β’ (((π₯(ballβπ)((π₯ππ¦) / 2)) β (MetOpenβπ) β§ (π¦(ballβπ)((π₯ππ¦) / 2)) β (MetOpenβπ) β§ (π₯ β (π₯(ballβπ)((π₯ππ¦) / 2)) β§ π¦ β (π¦(ballβπ)((π₯ππ¦) / 2)) β§ ((π₯(ballβπ)((π₯ππ¦) / 2)) β© (π¦(ballβπ)((π₯ππ¦) / 2))) = β
)) β βπ β (MetOpenβπ)βπ β (MetOpenβπ)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
43 | 17, 20, 22, 24, 33, 42 | syl113anc 1383 |
. . . . . . 7
β’ (((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β§ π₯ β π¦) β βπ β (MetOpenβπ)βπ β (MetOpenβπ)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
44 | 43 | ex 414 |
. . . . . 6
β’ ((π β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯ β π¦ β βπ β (MetOpenβπ)βπ β (MetOpenβπ)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
45 | 44 | ralrimivva 3198 |
. . . . 5
β’ (π β (Metβπ) β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β (MetOpenβπ)βπ β (MetOpenβπ)(π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
46 | 15 | mopntopon 23808 |
. . . . . 6
β’ (π β (βMetβπ) β (MetOpenβπ) β (TopOnβπ)) |
47 | | ishaus2 22718 |
. . . . . 6
β’
((MetOpenβπ)
β (TopOnβπ)
β ((MetOpenβπ)
β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β (MetOpenβπ)βπ β (MetOpenβπ)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
48 | 3, 46, 47 | 3syl 18 |
. . . . 5
β’ (π β (Metβπ) β ((MetOpenβπ) β Haus β
βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β (MetOpenβπ)βπ β (MetOpenβπ)(π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
49 | 45, 48 | mpbird 257 |
. . . 4
β’ (π β (Metβπ) β (MetOpenβπ) β Haus) |
50 | | eleq1 2826 |
. . . 4
β’ (π½ = (MetOpenβπ) β (π½ β Haus β (MetOpenβπ) β Haus)) |
51 | 49, 50 | syl5ibrcom 247 |
. . 3
β’ (π β (Metβπ) β (π½ = (MetOpenβπ) β π½ β Haus)) |
52 | 51 | rexlimiv 3146 |
. 2
β’
(βπ β
(Metβπ)π½ = (MetOpenβπ) β π½ β Haus) |
53 | 2, 52 | syl 17 |
1
β’ (π· β (βMetβπ) β π½ β Haus) |