Step | Hyp | Ref
| Expression |
1 | | eqid 2727 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
2 | 1 | cldss 22907 |
. . . . . 6
β’ (π₯ β (Clsdβπ½) β π₯ β βͺ π½) |
3 | 2 | adantl 481 |
. . . . 5
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β π₯ β βͺ π½) |
4 | | dfss4 4254 |
. . . . 5
β’ (π₯ β βͺ π½
β (βͺ π½ β (βͺ π½ β π₯)) = π₯) |
5 | 3, 4 | sylib 217 |
. . . 4
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β (βͺ π½ β π₯)) = π₯) |
6 | 1 | topopn 22782 |
. . . . . 6
β’ (π½ β Top β βͺ π½
β π½) |
7 | 1 | difopn 22912 |
. . . . . 6
β’ ((βͺ π½
β π½ β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯) β π½) |
8 | 6, 7 | sylan 579 |
. . . . 5
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯) β π½) |
9 | | id 22 |
. . . . . . . 8
β’ (π½ β Top β π½ β Top) |
10 | 9 | sgsiga 33684 |
. . . . . . 7
β’ (π½ β Top β
(sigaGenβπ½) β
βͺ ran sigAlgebra) |
11 | 10 | adantr 480 |
. . . . . 6
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β (sigaGenβπ½) β βͺ ran sigAlgebra) |
12 | | elex 3488 |
. . . . . . . 8
β’ (π½ β Top β π½ β V) |
13 | | sigagensiga 33683 |
. . . . . . . 8
β’ (π½ β V β
(sigaGenβπ½) β
(sigAlgebraββͺ π½)) |
14 | | baselsiga 33657 |
. . . . . . . 8
β’
((sigaGenβπ½)
β (sigAlgebraββͺ π½) β βͺ π½ β (sigaGenβπ½)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . 7
β’ (π½ β Top β βͺ π½
β (sigaGenβπ½)) |
16 | 15 | adantr 480 |
. . . . . 6
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β βͺ π½
β (sigaGenβπ½)) |
17 | | elsigagen 33689 |
. . . . . 6
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β (βͺ π½
β π₯) β
(sigaGenβπ½)) |
18 | | difelsiga 33675 |
. . . . . 6
β’
(((sigaGenβπ½)
β βͺ ran sigAlgebra β§ βͺ π½
β (sigaGenβπ½)
β§ (βͺ π½ β π₯) β (sigaGenβπ½)) β (βͺ
π½ β (βͺ π½
β π₯)) β
(sigaGenβπ½)) |
19 | 11, 16, 17, 18 | syl3anc 1369 |
. . . . 5
β’ ((π½ β Top β§ (βͺ π½
β π₯) β π½) β (βͺ π½
β (βͺ π½ β π₯)) β (sigaGenβπ½)) |
20 | 8, 19 | syldan 590 |
. . . 4
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β (βͺ π½ β π₯)) β (sigaGenβπ½)) |
21 | 5, 20 | eqeltrrd 2829 |
. . 3
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β π₯ β (sigaGenβπ½)) |
22 | 21 | ex 412 |
. 2
β’ (π½ β Top β (π₯ β (Clsdβπ½) β π₯ β (sigaGenβπ½))) |
23 | 22 | ssrdv 3984 |
1
β’ (π½ β Top β
(Clsdβπ½) β
(sigaGenβπ½)) |