Step | Hyp | Ref
| Expression |
1 | | ishaus2 23075 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
2 | | topontop 22635 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
3 | | simp1 1134 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β π½ β§ π β π½) β π½ β Top) |
4 | | simp2 1135 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β π½ β§ π β π½) β π β π½) |
5 | | simp1 1134 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π β§ (π β© π) = β
) β π₯ β π) |
6 | | opnneip 22843 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β π½ β§ π₯ β π) β π β ((neiβπ½)β{π₯})) |
7 | 3, 4, 5, 6 | syl2an3an 1420 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β π½ β§ π β π½) β§ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β π β ((neiβπ½)β{π₯})) |
8 | | simp3 1136 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β π½ β§ π β π½) β π β π½) |
9 | | simp2 1135 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π β§ (π β© π) = β
) β π¦ β π) |
10 | | opnneip 22843 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β π½ β§ π¦ β π) β π β ((neiβπ½)β{π¦})) |
11 | 3, 8, 9, 10 | syl2an3an 1420 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β π½ β§ π β π½) β§ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β π β ((neiβπ½)β{π¦})) |
12 | | simpr3 1194 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β π½ β§ π β π½) β§ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β (π β© π) = β
) |
13 | | ineq1 4204 |
. . . . . . . . . . . 12
β’ (π’ = π β (π’ β© π£) = (π β© π£)) |
14 | 13 | eqeq1d 2732 |
. . . . . . . . . . 11
β’ (π’ = π β ((π’ β© π£) = β
β (π β© π£) = β
)) |
15 | | ineq2 4205 |
. . . . . . . . . . . 12
β’ (π£ = π β (π β© π£) = (π β© π)) |
16 | 15 | eqeq1d 2732 |
. . . . . . . . . . 11
β’ (π£ = π β ((π β© π£) = β
β (π β© π) = β
)) |
17 | 14, 16 | rspc2ev 3623 |
. . . . . . . . . 10
β’ ((π β ((neiβπ½)β{π₯}) β§ π β ((neiβπ½)β{π¦}) β§ (π β© π) = β
) β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
) |
18 | 7, 11, 12, 17 | syl3anc 1369 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β π½ β§ π β π½) β§ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
) |
19 | 18 | ex 411 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π½ β§ π β π½) β ((π₯ β π β§ π¦ β π β§ (π β© π) = β
) β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
)) |
20 | 19 | 3expib 1120 |
. . . . . . 7
β’ (π½ β Top β ((π β π½ β§ π β π½) β ((π₯ β π β§ π¦ β π β§ (π β© π) = β
) β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
))) |
21 | 20 | rexlimdvv 3208 |
. . . . . 6
β’ (π½ β Top β (βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
) β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
)) |
22 | | neii2 22832 |
. . . . . . . . 9
β’ ((π½ β Top β§ π’ β ((neiβπ½)β{π₯})) β βπ β π½ ({π₯} β π β§ π β π’)) |
23 | 22 | ex 411 |
. . . . . . . 8
β’ (π½ β Top β (π’ β ((neiβπ½)β{π₯}) β βπ β π½ ({π₯} β π β§ π β π’))) |
24 | | neii2 22832 |
. . . . . . . . 9
β’ ((π½ β Top β§ π£ β ((neiβπ½)β{π¦})) β βπ β π½ ({π¦} β π β§ π β π£)) |
25 | 24 | ex 411 |
. . . . . . . 8
β’ (π½ β Top β (π£ β ((neiβπ½)β{π¦}) β βπ β π½ ({π¦} β π β§ π β π£))) |
26 | | vex 3476 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
27 | 26 | snss 4788 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β {π₯} β π) |
28 | 27 | anbi1i 622 |
. . . . . . . . . . . . 13
β’ ((π₯ β π β§ π β π’) β ({π₯} β π β§ π β π’)) |
29 | | vex 3476 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π¦ β V |
30 | 29 | snss 4788 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β π β {π¦} β π) |
31 | 30 | anbi1i 622 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ β π β§ π β π£) β ({π¦} β π β§ π β π£)) |
32 | | simp1l 1195 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β π β§ π β π’) β§ (π¦ β π β§ π β π£) β§ (π’ β© π£) = β
) β π₯ β π) |
33 | | simp2l 1197 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β π β§ π β π’) β§ (π¦ β π β§ π β π£) β§ (π’ β© π£) = β
) β π¦ β π) |
34 | | ss2in 4235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π’ β§ π β π£) β (π β© π) β (π’ β© π£)) |
35 | | ssn0 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β© π) β (π’ β© π£) β§ (π β© π) β β
) β (π’ β© π£) β β
) |
36 | 35 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β© π) β (π’ β© π£) β ((π β© π) β β
β (π’ β© π£) β β
)) |
37 | 36 | necon4d 2962 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β© π) β (π’ β© π£) β ((π’ β© π£) = β
β (π β© π) = β
)) |
38 | 34, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π’ β§ π β π£) β ((π’ β© π£) = β
β (π β© π) = β
)) |
39 | 38 | ad2ant2l 742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π₯ β π β§ π β π’) β§ (π¦ β π β§ π β π£)) β ((π’ β© π£) = β
β (π β© π) = β
)) |
40 | 39 | 3impia 1115 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β π β§ π β π’) β§ (π¦ β π β§ π β π£) β§ (π’ β© π£) = β
) β (π β© π) = β
) |
41 | 32, 33, 40 | 3jca 1126 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β π β§ π β π’) β§ (π¦ β π β§ π β π£) β§ (π’ β© π£) = β
) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) |
42 | 41 | 3exp 1117 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β π β§ π β π’) β ((π¦ β π β§ π β π£) β ((π’ β© π£) = β
β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
43 | 31, 42 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β π β§ π β π’) β (({π¦} β π β§ π β π£) β ((π’ β© π£) = β
β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
44 | 43 | com3r 87 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π’ β© π£) = β
β ((π₯ β π β§ π β π’) β (({π¦} β π β§ π β π£) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
45 | 44 | imp 405 |
. . . . . . . . . . . . . . . . . 18
β’ (((π’ β© π£) = β
β§ (π₯ β π β§ π β π’)) β (({π¦} β π β§ π β π£) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
46 | 45 | 3adant1 1128 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ (π’ β© π£) = β
β§ (π₯ β π β§ π β π’)) β (({π¦} β π β§ π β π£) β (π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
47 | 46 | reximdv 3168 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ (π’ β© π£) = β
β§ (π₯ β π β§ π β π’)) β (βπ β π½ ({π¦} β π β§ π β π£) β βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
48 | 47 | 3exp 1117 |
. . . . . . . . . . . . . . 15
β’ (π½ β Top β ((π’ β© π£) = β
β ((π₯ β π β§ π β π’) β (βπ β π½ ({π¦} β π β§ π β π£) β βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))))) |
49 | 48 | com34 91 |
. . . . . . . . . . . . . 14
β’ (π½ β Top β ((π’ β© π£) = β
β (βπ β π½ ({π¦} β π β§ π β π£) β ((π₯ β π β§ π β π’) β βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))))) |
50 | 49 | 3imp 1109 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ (π’ β© π£) = β
β§ βπ β π½ ({π¦} β π β§ π β π£)) β ((π₯ β π β§ π β π’) β βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
51 | 28, 50 | biimtrrid 242 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ (π’ β© π£) = β
β§ βπ β π½ ({π¦} β π β§ π β π£)) β (({π₯} β π β§ π β π’) β βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
52 | 51 | reximdv 3168 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ (π’ β© π£) = β
β§ βπ β π½ ({π¦} β π β§ π β π£)) β (βπ β π½ ({π₯} β π β§ π β π’) β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
53 | 52 | 3exp 1117 |
. . . . . . . . . 10
β’ (π½ β Top β ((π’ β© π£) = β
β (βπ β π½ ({π¦} β π β§ π β π£) β (βπ β π½ ({π₯} β π β§ π β π’) β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))))) |
54 | 53 | com24 95 |
. . . . . . . . 9
β’ (π½ β Top β (βπ β π½ ({π₯} β π β§ π β π’) β (βπ β π½ ({π¦} β π β§ π β π£) β ((π’ β© π£) = β
β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))))) |
55 | 54 | impd 409 |
. . . . . . . 8
β’ (π½ β Top β
((βπ β π½ ({π₯} β π β§ π β π’) β§ βπ β π½ ({π¦} β π β§ π β π£)) β ((π’ β© π£) = β
β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
56 | 23, 25, 55 | syl2and 606 |
. . . . . . 7
β’ (π½ β Top β ((π’ β ((neiβπ½)β{π₯}) β§ π£ β ((neiβπ½)β{π¦})) β ((π’ β© π£) = β
β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)))) |
57 | 56 | rexlimdvv 3208 |
. . . . . 6
β’ (π½ β Top β (βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
))) |
58 | 21, 57 | impbid 211 |
. . . . 5
β’ (π½ β Top β (βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
) β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
)) |
59 | 58 | imbi2d 339 |
. . . 4
β’ (π½ β Top β ((π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β (π₯ β π¦ β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
))) |
60 | 59 | 2ralbidv 3216 |
. . 3
β’ (π½ β Top β
(βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
))) |
61 | 2, 60 | syl 17 |
. 2
β’ (π½ β (TopOnβπ) β (βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β
)) β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
))) |
62 | 1, 61 | bitrd 278 |
1
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β
))) |