Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
2 | 1 | cldss 22396 |
. . . . . 6
β’ (π₯ β (Clsdβπ½) β π₯ β βͺ π½) |
3 | 2 | adantl 483 |
. . . . 5
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β π₯ β βͺ π½) |
4 | | dfss4 4223 |
. . . . 5
β’ (π₯ β βͺ π½
β (βͺ π½ β (βͺ π½ β π₯)) = π₯) |
5 | 3, 4 | sylib 217 |
. . . 4
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β (βͺ π½ β π₯)) = π₯) |
6 | 1 | topopn 22271 |
. . . . . 6
β’ (π½ β Top β βͺ π½
β π½) |
7 | 1 | difopn 22401 |
. . . . . 6
β’ ((βͺ π½
β π½ β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯) β π½) |
8 | 6, 7 | sylan 581 |
. . . . 5
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯) β π½) |
9 | | id 22 |
. . . . . . . 8
β’ (π½ β Top β π½ β Top) |
10 | 9 | sgsiga 32781 |
. . . . . . 7
β’ (π½ β Top β
(sigaGenβπ½) β
βͺ ran sigAlgebra) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β (sigaGenβπ½) β βͺ ran sigAlgebra) |
12 | | elex 3466 |
. . . . . . . 8
β’ (π½ β Top β π½ β V) |
13 | | sigagensiga 32780 |
. . . . . . . 8
β’ (π½ β V β
(sigaGenβπ½) β
(sigAlgebraββͺ π½)) |
14 | | baselsiga 32754 |
. . . . . . . 8
β’
((sigaGenβπ½)
β (sigAlgebraββͺ π½) β βͺ π½ β (sigaGenβπ½)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . 7
β’ (π½ β Top β βͺ π½
β (sigaGenβπ½)) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β βͺ π½
β (sigaGenβπ½)) |
17 | | elsigagen 32786 |
. . . . . 6
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β (βͺ π½
β π₯) β
(sigaGenβπ½)) |
18 | | difelsiga 32772 |
. . . . . 6
β’
(((sigaGenβπ½)
β βͺ ran sigAlgebra β§ βͺ π½
β (sigaGenβπ½)
β§ (βͺ π½ β π₯) β (sigaGenβπ½)) β (βͺ
π½ β (βͺ π½
β π₯)) β
(sigaGenβπ½)) |
19 | 11, 16, 17, 18 | syl3anc 1372 |
. . . . 5
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β (βͺ π½
β (βͺ π½ β π₯)) β (sigaGenβπ½)) |
20 | 8, 19 | syldan 592 |
. . . 4
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β (βͺ π½ β π₯)) β (sigaGenβπ½)) |
21 | 5, 20 | eqeltrrd 2839 |
. . 3
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β π₯ β (sigaGenβπ½)) |
22 | 21 | ex 414 |
. 2
β’ (π½ β Top β (π₯ β (Clsdβπ½) β π₯ β (sigaGenβπ½))) |
23 | 22 | ssrdv 3955 |
1
β’ (π½ β Top β
(Clsdβπ½) β
(sigaGenβπ½)) |