Step |
Hyp |
Ref |
Expression |
1 |
|
kgenval |
β’ ( π½ β ( TopOn β π ) β ( πGen β π½ ) = { π₯ β π« π β£ β π β π« π ( ( π½ βΎt π ) β Comp β ( π₯ β© π ) β ( π½ βΎt π ) ) } ) |
2 |
1
|
eleq2d |
β’ ( π½ β ( TopOn β π ) β ( π΄ β ( πGen β π½ ) β π΄ β { π₯ β π« π β£ β π β π« π ( ( π½ βΎt π ) β Comp β ( π₯ β© π ) β ( π½ βΎt π ) ) } ) ) |
3 |
|
ineq1 |
β’ ( π₯ = π΄ β ( π₯ β© π ) = ( π΄ β© π ) ) |
4 |
3
|
eleq1d |
β’ ( π₯ = π΄ β ( ( π₯ β© π ) β ( π½ βΎt π ) β ( π΄ β© π ) β ( π½ βΎt π ) ) ) |
5 |
4
|
imbi2d |
β’ ( π₯ = π΄ β ( ( ( π½ βΎt π ) β Comp β ( π₯ β© π ) β ( π½ βΎt π ) ) β ( ( π½ βΎt π ) β Comp β ( π΄ β© π ) β ( π½ βΎt π ) ) ) ) |
6 |
5
|
ralbidv |
β’ ( π₯ = π΄ β ( β π β π« π ( ( π½ βΎt π ) β Comp β ( π₯ β© π ) β ( π½ βΎt π ) ) β β π β π« π ( ( π½ βΎt π ) β Comp β ( π΄ β© π ) β ( π½ βΎt π ) ) ) ) |
7 |
6
|
elrab |
β’ ( π΄ β { π₯ β π« π β£ β π β π« π ( ( π½ βΎt π ) β Comp β ( π₯ β© π ) β ( π½ βΎt π ) ) } β ( π΄ β π« π β§ β π β π« π ( ( π½ βΎt π ) β Comp β ( π΄ β© π ) β ( π½ βΎt π ) ) ) ) |
8 |
|
toponmax |
β’ ( π½ β ( TopOn β π ) β π β π½ ) |
9 |
|
elpw2g |
β’ ( π β π½ β ( π΄ β π« π β π΄ β π ) ) |
10 |
8 9
|
syl |
β’ ( π½ β ( TopOn β π ) β ( π΄ β π« π β π΄ β π ) ) |
11 |
10
|
anbi1d |
β’ ( π½ β ( TopOn β π ) β ( ( π΄ β π« π β§ β π β π« π ( ( π½ βΎt π ) β Comp β ( π΄ β© π ) β ( π½ βΎt π ) ) ) β ( π΄ β π β§ β π β π« π ( ( π½ βΎt π ) β Comp β ( π΄ β© π ) β ( π½ βΎt π ) ) ) ) ) |
12 |
7 11
|
bitrid |
β’ ( π½ β ( TopOn β π ) β ( π΄ β { π₯ β π« π β£ β π β π« π ( ( π½ βΎt π ) β Comp β ( π₯ β© π ) β ( π½ βΎt π ) ) } β ( π΄ β π β§ β π β π« π ( ( π½ βΎt π ) β Comp β ( π΄ β© π ) β ( π½ βΎt π ) ) ) ) ) |
13 |
2 12
|
bitrd |
β’ ( π½ β ( TopOn β π ) β ( π΄ β ( πGen β π½ ) β ( π΄ β π β§ β π β π« π ( ( π½ βΎt π ) β Comp β ( π΄ β© π ) β ( π½ βΎt π ) ) ) ) ) |