Step | Hyp | Ref
| Expression |
1 | | eqid 2730 |
. . . 4
β’ {π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))} = {π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))} |
2 | 1 | ptbas 23305 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β {π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))} β TopBases) |
3 | | unitg 22692 |
. . 3
β’ ({π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))} β TopBases β βͺ (topGenβ{π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))}) = βͺ {π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))}) |
4 | 2, 3 | syl 17 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β βͺ (topGenβ{π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))}) = βͺ {π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))}) |
5 | | ptuni.1 |
. . . 4
β’ π½ =
(βtβπΉ) |
6 | | ffn 6718 |
. . . . 5
β’ (πΉ:π΄βΆTop β πΉ Fn π΄) |
7 | 1 | ptval 23296 |
. . . . 5
β’ ((π΄ β π β§ πΉ Fn π΄) β (βtβπΉ) = (topGenβ{π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))})) |
8 | 6, 7 | sylan2 591 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β
(βtβπΉ) = (topGenβ{π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))})) |
9 | 5, 8 | eqtrid 2782 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β π½ = (topGenβ{π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))})) |
10 | 9 | unieqd 4923 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β βͺ π½ =
βͺ (topGenβ{π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))})) |
11 | 1 | ptuni2 23302 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ₯ β
π΄ βͺ (πΉβπ₯) = βͺ {π β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))}) |
12 | 4, 10, 11 | 3eqtr4rd 2781 |
1
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ₯ β
π΄ βͺ (πΉβπ₯) = βͺ π½) |