Step | Hyp | Ref
| Expression |
1 | | topmtcl 35248 |
. . . 4
β’ ((π β π β§ π β (TopOnβπ)) β (π« π β© β© π) β (TopOnβπ)) |
2 | | inss2 4230 |
. . . . . . 7
β’
(π« π β©
β© π) β β© π |
3 | | intss1 4968 |
. . . . . . 7
β’ (π β π β β© π β π) |
4 | 2, 3 | sstrid 3994 |
. . . . . 6
β’ (π β π β (π« π β© β© π) β π) |
5 | 4 | rgen 3064 |
. . . . 5
β’
βπ β
π (π« π β© β© π)
β π |
6 | | sseq1 4008 |
. . . . . . 7
β’ (π = (π« π β© β© π) β (π β π β (π« π β© β© π) β π)) |
7 | 6 | ralbidv 3178 |
. . . . . 6
β’ (π = (π« π β© β© π) β (βπ β π π β π β βπ β π (π« π β© β© π) β π)) |
8 | 7 | elrab 3684 |
. . . . 5
β’
((π« π β©
β© π) β {π β (TopOnβπ) β£ βπ β π π β π} β ((π« π β© β© π) β (TopOnβπ) β§ βπ β π (π« π β© β© π) β π)) |
9 | 5, 8 | mpbiran2 709 |
. . . 4
β’
((π« π β©
β© π) β {π β (TopOnβπ) β£ βπ β π π β π} β (π« π β© β© π) β (TopOnβπ)) |
10 | 1, 9 | sylibr 233 |
. . 3
β’ ((π β π β§ π β (TopOnβπ)) β (π« π β© β© π) β {π β (TopOnβπ) β£ βπ β π π β π}) |
11 | | elssuni 4942 |
. . 3
β’
((π« π β©
β© π) β {π β (TopOnβπ) β£ βπ β π π β π} β (π« π β© β© π) β βͺ {π
β (TopOnβπ)
β£ βπ β
π π β π}) |
12 | 10, 11 | syl 17 |
. 2
β’ ((π β π β§ π β (TopOnβπ)) β (π« π β© β© π) β βͺ {π
β (TopOnβπ)
β£ βπ β
π π β π}) |
13 | | toponuni 22416 |
. . . . . . . . 9
β’ (π β (TopOnβπ) β π = βͺ π) |
14 | | eqimss2 4042 |
. . . . . . . . 9
β’ (π = βͺ
π β βͺ π
β π) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
β’ (π β (TopOnβπ) β βͺ π
β π) |
16 | | sspwuni 5104 |
. . . . . . . 8
β’ (π β π« π β βͺ π
β π) |
17 | 15, 16 | sylibr 233 |
. . . . . . 7
β’ (π β (TopOnβπ) β π β π« π) |
18 | 17 | 3ad2ant2 1135 |
. . . . . 6
β’ (((π β π β§ π β (TopOnβπ)) β§ π β (TopOnβπ) β§ βπ β π π β π) β π β π« π) |
19 | | simp3 1139 |
. . . . . . 7
β’ (((π β π β§ π β (TopOnβπ)) β§ π β (TopOnβπ) β§ βπ β π π β π) β βπ β π π β π) |
20 | | ssint 4969 |
. . . . . . 7
β’ (π β β© π
β βπ β
π π β π) |
21 | 19, 20 | sylibr 233 |
. . . . . 6
β’ (((π β π β§ π β (TopOnβπ)) β§ π β (TopOnβπ) β§ βπ β π π β π) β π β β© π) |
22 | 18, 21 | ssind 4233 |
. . . . 5
β’ (((π β π β§ π β (TopOnβπ)) β§ π β (TopOnβπ) β§ βπ β π π β π) β π β (π« π β© β© π)) |
23 | | velpw 4608 |
. . . . 5
β’ (π β π« (π«
π β© β© π)
β π β (π«
π β© β© π)) |
24 | 22, 23 | sylibr 233 |
. . . 4
β’ (((π β π β§ π β (TopOnβπ)) β§ π β (TopOnβπ) β§ βπ β π π β π) β π β π« (π« π β© β© π)) |
25 | 24 | rabssdv 4073 |
. . 3
β’ ((π β π β§ π β (TopOnβπ)) β {π β (TopOnβπ) β£ βπ β π π β π} β π« (π« π β© β© π)) |
26 | | sspwuni 5104 |
. . 3
β’ ({π β (TopOnβπ) β£ βπ β π π β π} β π« (π« π β© β© π)
β βͺ {π β (TopOnβπ) β£ βπ β π π β π} β (π« π β© β© π)) |
27 | 25, 26 | sylib 217 |
. 2
β’ ((π β π β§ π β (TopOnβπ)) β βͺ
{π β
(TopOnβπ) β£
βπ β π π β π} β (π« π β© β© π)) |
28 | 12, 27 | eqssd 4000 |
1
β’ ((π β π β§ π β (TopOnβπ)) β (π« π β© β© π) = βͺ
{π β
(TopOnβπ) β£
βπ β π π β π}) |