| Step | Hyp | Ref
| Expression |
|---|
| 1 | | prex 5431 |
. . . . 5
β’ {π, {π« βͺ π}}
β V |
| 2 | | vex 3478 |
. . . . . . . 8
β’ π₯ β V |
| 3 | 2 | elpr 4650 |
. . . . . . 7
β’ (π₯ β {π, {π« βͺ
π}} β (π₯ = π β¨ π₯ = {π« βͺ
π})) |
| 4 | | vex 3478 |
. . . . . . . 8
β’ π¦ β V |
| 5 | 4 | elpr 4650 |
. . . . . . 7
β’ (π¦ β {π, {π« βͺ
π}} β (π¦ = π β¨ π¦ = {π« βͺ
π})) |
| 6 | | eqtr3 2758 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π) β π₯ = π¦) |
| 7 | 6 | orcd 871 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π) β (π₯ = π¦ β¨ (π₯ β© π¦) = β
)) |
| 8 | | ineq12 4206 |
. . . . . . . . . 10
β’ ((π₯ = {π« βͺ π}
β§ π¦ = π) β (π₯ β© π¦) = ({π« βͺ
π} β© π)) |
| 9 | | incom 4200 |
. . . . . . . . . . 11
β’
({π« βͺ π} β© π) = (π β© {π« βͺ π}) |
| 10 | | pwuninel 8256 |
. . . . . . . . . . . 12
β’ Β¬
π« βͺ π β π |
| 11 | | disjsn 4714 |
. . . . . . . . . . . 12
β’ ((π β© {π« βͺ π})
= β
β Β¬ π« βͺ π β π) |
| 12 | 10, 11 | mpbir 230 |
. . . . . . . . . . 11
β’ (π β© {π« βͺ π})
= β
|
| 13 | 9, 12 | eqtri 2760 |
. . . . . . . . . 10
β’
({π« βͺ π} β© π) = β
|
| 14 | 8, 13 | eqtrdi 2788 |
. . . . . . . . 9
β’ ((π₯ = {π« βͺ π}
β§ π¦ = π) β (π₯ β© π¦) = β
) |
| 15 | 14 | olcd 872 |
. . . . . . . 8
β’ ((π₯ = {π« βͺ π}
β§ π¦ = π) β (π₯ = π¦ β¨ (π₯ β© π¦) = β
)) |
| 16 | | ineq12 4206 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = {π« βͺ
π}) β (π₯ β© π¦) = (π β© {π« βͺ π})) |
| 17 | 16, 12 | eqtrdi 2788 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = {π« βͺ
π}) β (π₯ β© π¦) = β
) |
| 18 | 17 | olcd 872 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = {π« βͺ
π}) β (π₯ = π¦ β¨ (π₯ β© π¦) = β
)) |
| 19 | | eqtr3 2758 |
. . . . . . . . 9
β’ ((π₯ = {π« βͺ π}
β§ π¦ = {π« βͺ π})
β π₯ = π¦) |
| 20 | 19 | orcd 871 |
. . . . . . . 8
β’ ((π₯ = {π« βͺ π}
β§ π¦ = {π« βͺ π})
β (π₯ = π¦ β¨ (π₯ β© π¦) = β
)) |
| 21 | 7, 15, 18, 20 | ccase 1036 |
. . . . . . 7
β’ (((π₯ = π β¨ π₯ = {π« βͺ
π}) β§ (π¦ = π β¨ π¦ = {π« βͺ
π})) β (π₯ = π¦ β¨ (π₯ β© π¦) = β
)) |
| 22 | 3, 5, 21 | syl2anb 598 |
. . . . . 6
β’ ((π₯ β {π, {π« βͺ
π}} β§ π¦ β {π, {π« βͺ
π}}) β (π₯ = π¦ β¨ (π₯ β© π¦) = β
)) |
| 23 | 22 | rgen2 3197 |
. . . . 5
β’
βπ₯ β
{π, {π« βͺ π}}βπ¦ β {π, {π« βͺ
π}} (π₯ = π¦ β¨ (π₯ β© π¦) = β
) |
| 24 | | baspartn 22448 |
. . . . 5
β’ (({π, {π« βͺ π}}
β V β§ βπ₯
β {π, {π« βͺ π}}βπ¦ β {π, {π« βͺ
π}} (π₯ = π¦ β¨ (π₯ β© π¦) = β
)) β {π, {π« βͺ
π}} β
TopBases) |
| 25 | 1, 23, 24 | mp2an 690 |
. . . 4
β’ {π, {π« βͺ π}}
β TopBases |
| 26 | | tgcl 22463 |
. . . 4
β’ ({π, {π« βͺ π}}
β TopBases β (topGenβ{π, {π« βͺ
π}}) β
Top) |
| 27 | 25, 26 | mp1i 13 |
. . 3
β’ (π β π β (topGenβ{π, {π« βͺ
π}}) β
Top) |
| 28 | | prfi 9318 |
. . . . . 6
β’ {π, {π« βͺ π}}
β Fin |
| 29 | | pwfi 9174 |
. . . . . 6
β’ ({π, {π« βͺ π}}
β Fin β π« {π, {π« βͺ
π}} β
Fin) |
| 30 | 28, 29 | mpbi 229 |
. . . . 5
β’ π«
{π, {π« βͺ π}}
β Fin |
| 31 | | tgdom 22472 |
. . . . . 6
β’ ({π, {π« βͺ π}}
β V β (topGenβ{π, {π« βͺ
π}}) βΌ π«
{π, {π« βͺ π}}) |
| 32 | 1, 31 | ax-mp 5 |
. . . . 5
β’
(topGenβ{π,
{π« βͺ π}}) βΌ π« {π, {π« βͺ
π}} |
| 33 | | domfi 9188 |
. . . . 5
β’
((π« {π,
{π« βͺ π}} β Fin β§ (topGenβ{π, {π« βͺ π}})
βΌ π« {π,
{π« βͺ π}}) β (topGenβ{π, {π« βͺ
π}}) β
Fin) |
| 34 | 30, 32, 33 | mp2an 690 |
. . . 4
β’
(topGenβ{π,
{π« βͺ π}}) β Fin |
| 35 | 34 | a1i 11 |
. . 3
β’ (π β π β (topGenβ{π, {π« βͺ
π}}) β
Fin) |
| 36 | 27, 35 | elind 4193 |
. 2
β’ (π β π β (topGenβ{π, {π« βͺ
π}}) β (Top β©
Fin)) |
| 37 | | fincmp 22888 |
. 2
β’
((topGenβ{π,
{π« βͺ π}}) β (Top β© Fin) β
(topGenβ{π,
{π« βͺ π}}) β Comp) |
| 38 | 36, 37 | syl 17 |
1
β’ (π β π β (topGenβ{π, {π« βͺ
π}}) β
Comp) |
