Step | Hyp | Ref
| Expression |
1 | | ismntoplly 33000 |
. 2
β’ ((π β β0
β§ π½ β π) β (πManTopπ½ β (π½ β 2ndΟ β§ π½ β Haus β§ π½ β Locally
[(TopOpenβ(πΌhilβπ))] β ))) |
2 | | haustop 22834 |
. . . . . . . . 9
β’ (π½ β Haus β π½ β Top) |
3 | 2 | adantl 482 |
. . . . . . . 8
β’ ((π β β0
β§ π½ β Haus) β
π½ β
Top) |
4 | 3 | biantrurd 533 |
. . . . . . 7
β’ ((π β β0
β§ π½ β Haus) β
(βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β ) β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β )))) |
5 | | hmpher 23287 |
. . . . . . . . . . . . 13
β’ β
Er Top |
6 | | errel 8711 |
. . . . . . . . . . . . 13
β’ ( β
Er Top β Rel β ) |
7 | | relelec 8747 |
. . . . . . . . . . . . 13
β’ (Rel
β β ((π½
βΎt π’)
β [(TopOpenβ(πΌhilβπ))] β β
(TopOpenβ(πΌhilβπ)) β (π½ βΎt π’))) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . . . . 12
β’ ((π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β β
(TopOpenβ(πΌhilβπ)) β (π½ βΎt π’)) |
9 | | hmphsymb 23289 |
. . . . . . . . . . . 12
β’
((TopOpenβ(πΌhilβπ)) β (π½ βΎt π’) β (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ))) |
10 | 8, 9 | bitr2i 275 |
. . . . . . . . . . 11
β’ ((π½ βΎt π’) β
(TopOpenβ(πΌhilβπ)) β (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β ) |
11 | 10 | a1i 11 |
. . . . . . . . . 10
β’ ((π β β0
β§ π½ β Haus) β
((π½ βΎt
π’) β
(TopOpenβ(πΌhilβπ)) β (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β )) |
12 | 11 | anbi2d 629 |
. . . . . . . . 9
β’ ((π β β0
β§ π½ β Haus) β
((π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ))) β (π¦ β π’ β§ (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β ))) |
13 | 12 | rexbidv 3178 |
. . . . . . . 8
β’ ((π β β0
β§ π½ β Haus) β
(βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ))) β βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β ))) |
14 | 13 | 2ralbidv 3218 |
. . . . . . 7
β’ ((π β β0
β§ π½ β Haus) β
(βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ))) β βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β ))) |
15 | | islly 22971 |
. . . . . . . 8
β’ (π½ β Locally
[(TopOpenβ(πΌhilβπ))] β β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β ))) |
16 | 15 | a1i 11 |
. . . . . . 7
β’ ((π β β0
β§ π½ β Haus) β
(π½ β Locally
[(TopOpenβ(πΌhilβπ))] β β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
[(TopOpenβ(πΌhilβπ))] β )))) |
17 | 4, 14, 16 | 3bitr4rd 311 |
. . . . . 6
β’ ((π β β0
β§ π½ β Haus) β
(π½ β Locally
[(TopOpenβ(πΌhilβπ))] β β βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ))))) |
18 | 17 | pm5.32da 579 |
. . . . 5
β’ (π β β0
β ((π½ β Haus
β§ π½ β Locally
[(TopOpenβ(πΌhilβπ))] β ) β (π½ β Haus β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ)))))) |
19 | 18 | anbi2d 629 |
. . . 4
β’ (π β β0
β ((π½ β
2ndΟ β§ (π½ β Haus β§ π½ β Locally
[(TopOpenβ(πΌhilβπ))] β )) β (π½ β 2ndΟ β§ (π½ β Haus β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ))))))) |
20 | | 3anass 1095 |
. . . 4
β’ ((π½ β 2ndΟ
β§ π½ β Haus β§
π½ β Locally
[(TopOpenβ(πΌhilβπ))] β ) β (π½ β 2ndΟ β§ (π½ β Haus β§ π½ β Locally
[(TopOpenβ(πΌhilβπ))] β ))) |
21 | | 3anass 1095 |
. . . 4
β’ ((π½ β 2ndΟ
β§ π½ β Haus β§
βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ)))) β (π½ β 2ndΟ β§ (π½ β Haus β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ)))))) |
22 | 19, 20, 21 | 3bitr4g 313 |
. . 3
β’ (π β β0
β ((π½ β
2ndΟ β§ π½ β Haus β§ π½ β Locally
[(TopOpenβ(πΌhilβπ))] β ) β (π½ β 2ndΟ β§ π½ β Haus β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ)))))) |
23 | 22 | adantr 481 |
. 2
β’ ((π β β0
β§ π½ β π) β ((π½ β 2ndΟ β§ π½ β Haus β§ π½ β Locally
[(TopOpenβ(πΌhilβπ))] β ) β (π½ β 2ndΟ β§ π½ β Haus β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ)))))) |
24 | 1, 23 | bitrd 278 |
1
β’ ((π β β0
β§ π½ β π) β (πManTopπ½ β (π½ β 2ndΟ β§ π½ β Haus β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β
(TopOpenβ(πΌhilβπ)))))) |