Step | Hyp | Ref
| Expression |
1 | | neibastop1.1 |
. . . 4
β’ (π β π β π) |
2 | | neibastop1.2 |
. . . 4
β’ (π β πΉ:πβΆ(π« π« π β
{β
})) |
3 | | neibastop1.3 |
. . . 4
β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β
) |
4 | | neibastop1.4 |
. . . 4
β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β
} |
5 | 1, 2, 3, 4 | neibastop1 34860 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
6 | | neibastop1.5 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) |
7 | | neibastop1.6 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
) |
8 | 1, 2, 3, 4, 6, 7 | neibastop2 34862 |
. . . . . . . 8
β’ ((π β§ π§ β π) β (π β ((neiβπ½)β{π§}) β (π β π β§ ((πΉβπ§) β© π« π) β β
))) |
9 | | velpw 4570 |
. . . . . . . . 9
β’ (π β π« π β π β π) |
10 | 9 | anbi1i 625 |
. . . . . . . 8
β’ ((π β π« π β§ ((πΉβπ§) β© π« π) β β
) β (π β π β§ ((πΉβπ§) β© π« π) β β
)) |
11 | 8, 10 | bitr4di 289 |
. . . . . . 7
β’ ((π β§ π§ β π) β (π β ((neiβπ½)β{π§}) β (π β π« π β§ ((πΉβπ§) β© π« π) β β
))) |
12 | 11 | abbi2dv 2872 |
. . . . . 6
β’ ((π β§ π§ β π) β ((neiβπ½)β{π§}) = {π β£ (π β π« π β§ ((πΉβπ§) β© π« π) β β
)}) |
13 | | df-rab 3411 |
. . . . . 6
β’ {π β π« π β£ ((πΉβπ§) β© π« π) β β
} = {π β£ (π β π« π β§ ((πΉβπ§) β© π« π) β β
)} |
14 | 12, 13 | eqtr4di 2795 |
. . . . 5
β’ ((π β§ π§ β π) β ((neiβπ½)β{π§}) = {π β π« π β£ ((πΉβπ§) β© π« π) β β
}) |
15 | 14 | ralrimiva 3144 |
. . . 4
β’ (π β βπ§ β π ((neiβπ½)β{π§}) = {π β π« π β£ ((πΉβπ§) β© π« π) β β
}) |
16 | | sneq 4601 |
. . . . . . 7
β’ (π₯ = π§ β {π₯} = {π§}) |
17 | 16 | fveq2d 6851 |
. . . . . 6
β’ (π₯ = π§ β ((neiβπ½)β{π₯}) = ((neiβπ½)β{π§})) |
18 | | fveq2 6847 |
. . . . . . . . 9
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
19 | 18 | ineq1d 4176 |
. . . . . . . 8
β’ (π₯ = π§ β ((πΉβπ₯) β© π« π) = ((πΉβπ§) β© π« π)) |
20 | 19 | neeq1d 3004 |
. . . . . . 7
β’ (π₯ = π§ β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ§) β© π« π) β β
)) |
21 | 20 | rabbidv 3418 |
. . . . . 6
β’ (π₯ = π§ β {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} = {π β π« π β£ ((πΉβπ§) β© π« π) β β
}) |
22 | 17, 21 | eqeq12d 2753 |
. . . . 5
β’ (π₯ = π§ β (((neiβπ½)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β ((neiβπ½)β{π§}) = {π β π« π β£ ((πΉβπ§) β© π« π) β β
})) |
23 | 22 | cbvralvw 3228 |
. . . 4
β’
(βπ₯ β
π ((neiβπ½)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β βπ§ β π ((neiβπ½)β{π§}) = {π β π« π β£ ((πΉβπ§) β© π« π) β β
}) |
24 | 15, 23 | sylibr 233 |
. . 3
β’ (π β βπ₯ β π ((neiβπ½)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) |
25 | | toponuni 22279 |
. . . . . . . . . 10
β’ (π β (TopOnβπ) β π = βͺ π) |
26 | | eqimss2 4006 |
. . . . . . . . . 10
β’ (π = βͺ
π β βͺ π
β π) |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
β’ (π β (TopOnβπ) β βͺ π
β π) |
28 | | sspwuni 5065 |
. . . . . . . . 9
β’ (π β π« π β βͺ π
β π) |
29 | 27, 28 | sylibr 233 |
. . . . . . . 8
β’ (π β (TopOnβπ) β π β π« π) |
30 | 29 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β π β π« π) |
31 | | sseqin2 4180 |
. . . . . . 7
β’ (π β π« π β (π« π β© π) = π) |
32 | 30, 31 | sylib 217 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β (π« π β© π) = π) |
33 | | topontop 22278 |
. . . . . . . . . . 11
β’ (π β (TopOnβπ) β π β Top) |
34 | 33 | ad3antlr 730 |
. . . . . . . . . 10
β’ ((((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β§ π β π« π) β π β Top) |
35 | | eltop2 22341 |
. . . . . . . . . 10
β’ (π β Top β (π β π β βπ₯ β π βπ§ β π (π₯ β π§ β§ π§ β π))) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β§ π β π« π) β (π β π β βπ₯ β π βπ§ β π (π₯ β π§ β§ π§ β π))) |
37 | | elpwi 4572 |
. . . . . . . . . . . . . . 15
β’ (π β π« π β π β π) |
38 | | ssralv 4015 |
. . . . . . . . . . . . . . 15
β’ (π β π β (βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π« π β (βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (TopOnβπ)) β§ π β π« π) β (βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
41 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) |
42 | 41 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β (π β ((neiβπ)β{π₯}) β π β {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
43 | 33 | ad3antlr 730 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β π β Top) |
44 | 25 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (TopOnβπ)) β π = βͺ π) |
45 | 44 | sseq2d 3981 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (TopOnβπ)) β (π β π β π β βͺ π)) |
46 | 45 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (TopOnβπ)) β§ π β π) β π β βͺ π) |
47 | 37, 46 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (TopOnβπ)) β§ π β π« π) β π β βͺ π) |
48 | 47 | sselda 3949 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ π₯ β π) β π₯ β βͺ π) |
49 | 48 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β π₯ β βͺ π) |
50 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β π β βͺ π) |
51 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’ βͺ π =
βͺ π |
52 | 51 | isneip 22472 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Top β§ π₯ β βͺ π)
β (π β
((neiβπ)β{π₯}) β (π β βͺ π β§ βπ§ β π (π₯ β π§ β§ π§ β π)))) |
53 | 52 | baibd 541 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Top β§ π₯ β βͺ π)
β§ π β βͺ π)
β (π β
((neiβπ)β{π₯}) β βπ§ β π (π₯ β π§ β§ π§ β π))) |
54 | 43, 49, 50, 53 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β (π β ((neiβπ)β{π₯}) β βπ§ β π (π₯ β π§ β§ π§ β π))) |
55 | | pweq 4579 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β π« π = π« π) |
56 | 55 | ineq2d 4177 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πΉβπ₯) β© π« π) = ((πΉβπ₯) β© π« π)) |
57 | 56 | neeq1d 3004 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
)) |
58 | 57 | elrab3 3651 |
. . . . . . . . . . . . . . . . 17
β’ (π β π« π β (π β {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β ((πΉβπ₯) β© π« π) β β
)) |
59 | 58 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β (π β {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β ((πΉβπ₯) β© π« π) β β
)) |
60 | 42, 54, 59 | 3bitr3d 309 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ (π₯ β π β§ ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) β (βπ§ β π (π₯ β π§ β§ π§ β π) β ((πΉβπ₯) β© π« π) β β
)) |
61 | 60 | expr 458 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ π₯ β π) β (((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β (βπ§ β π (π₯ β π§ β§ π§ β π) β ((πΉβπ₯) β© π« π) β β
))) |
62 | 61 | ralimdva 3165 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (TopOnβπ)) β§ π β π« π) β (βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β βπ₯ β π (βπ§ β π (π₯ β π§ β§ π§ β π) β ((πΉβπ₯) β© π« π) β β
))) |
63 | 40, 62 | syld 47 |
. . . . . . . . . . . 12
β’ (((π β§ π β (TopOnβπ)) β§ π β π« π) β (βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β βπ₯ β π (βπ§ β π (π₯ β π§ β§ π§ β π) β ((πΉβπ₯) β© π« π) β β
))) |
64 | 63 | imp 408 |
. . . . . . . . . . 11
β’ ((((π β§ π β (TopOnβπ)) β§ π β π« π) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β βπ₯ β π (βπ§ β π (π₯ β π§ β§ π§ β π) β ((πΉβπ₯) β© π« π) β β
)) |
65 | 64 | an32s 651 |
. . . . . . . . . 10
β’ ((((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β§ π β π« π) β βπ₯ β π (βπ§ β π (π₯ β π§ β§ π§ β π) β ((πΉβπ₯) β© π« π) β β
)) |
66 | | ralbi 3107 |
. . . . . . . . . 10
β’
(βπ₯ β
π (βπ§ β π (π₯ β π§ β§ π§ β π) β ((πΉβπ₯) β© π« π) β β
) β (βπ₯ β π βπ§ β π (π₯ β π§ β§ π§ β π) β βπ₯ β π ((πΉβπ₯) β© π« π) β β
)) |
67 | 65, 66 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β§ π β π« π) β (βπ₯ β π βπ§ β π (π₯ β π§ β§ π§ β π) β βπ₯ β π ((πΉβπ₯) β© π« π) β β
)) |
68 | 36, 67 | bitrd 279 |
. . . . . . . 8
β’ ((((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β§ π β π« π) β (π β π β βπ₯ β π ((πΉβπ₯) β© π« π) β β
)) |
69 | 68 | rabbi2dva 4182 |
. . . . . . 7
β’ (((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β (π« π β© π) = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β
}) |
70 | 69, 4 | eqtr4di 2795 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β (π« π β© π) = π½) |
71 | 32, 70 | eqtr3d 2779 |
. . . . 5
β’ (((π β§ π β (TopOnβπ)) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β π = π½) |
72 | 71 | expl 459 |
. . . 4
β’ (π β ((π β (TopOnβπ) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β π = π½)) |
73 | 72 | alrimiv 1931 |
. . 3
β’ (π β βπ((π β (TopOnβπ) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β π = π½)) |
74 | | eleq1 2826 |
. . . . 5
β’ (π = π½ β (π β (TopOnβπ) β π½ β (TopOnβπ))) |
75 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π½ β (neiβπ) = (neiβπ½)) |
76 | 75 | fveq1d 6849 |
. . . . . . 7
β’ (π = π½ β ((neiβπ)β{π₯}) = ((neiβπ½)β{π₯})) |
77 | 76 | eqeq1d 2739 |
. . . . . 6
β’ (π = π½ β (((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β ((neiβπ½)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
78 | 77 | ralbidv 3175 |
. . . . 5
β’ (π = π½ β (βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β βπ₯ β π ((neiβπ½)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
79 | 74, 78 | anbi12d 632 |
. . . 4
β’ (π = π½ β ((π β (TopOnβπ) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β (π½ β (TopOnβπ) β§ βπ₯ β π ((neiβπ½)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}))) |
80 | 79 | eqeu 3669 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (π½ β (TopOnβπ) β§ βπ₯ β π ((neiβπ½)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β§ βπ((π β (TopOnβπ) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) β π = π½)) β β!π(π β (TopOnβπ) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
81 | 5, 5, 24, 73, 80 | syl121anc 1376 |
. 2
β’ (π β β!π(π β (TopOnβπ) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
82 | | df-reu 3357 |
. 2
β’
(β!π β
(TopOnβπ)βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
} β β!π(π β (TopOnβπ) β§ βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
})) |
83 | 81, 82 | sylibr 233 |
1
β’ (π β β!π β (TopOnβπ)βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β
}) |