Step | Hyp | Ref
| Expression |
1 | | tgval 22321 |
. . 3
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) |
2 | 1 | eleq2d 2820 |
. 2
β’ (π΅ β π β (π΄ β (topGenβπ΅) β π΄ β {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)})) |
3 | | elex 3462 |
. . . 4
β’ (π΄ β {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)} β π΄ β V) |
4 | 3 | adantl 483 |
. . 3
β’ ((π΅ β π β§ π΄ β {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) β π΄ β V) |
5 | | inex1g 5277 |
. . . . . 6
β’ (π΅ β π β (π΅ β© π« π΄) β V) |
6 | 5 | uniexd 7680 |
. . . . 5
β’ (π΅ β π β βͺ (π΅ β© π« π΄) β V) |
7 | | ssexg 5281 |
. . . . 5
β’ ((π΄ β βͺ (π΅
β© π« π΄) β§
βͺ (π΅ β© π« π΄) β V) β π΄ β V) |
8 | 6, 7 | sylan2 594 |
. . . 4
β’ ((π΄ β βͺ (π΅
β© π« π΄) β§
π΅ β π) β π΄ β V) |
9 | 8 | ancoms 460 |
. . 3
β’ ((π΅ β π β§ π΄ β βͺ (π΅ β© π« π΄)) β π΄ β V) |
10 | | id 22 |
. . . . 5
β’ (π₯ = π΄ β π₯ = π΄) |
11 | | pweq 4575 |
. . . . . . 7
β’ (π₯ = π΄ β π« π₯ = π« π΄) |
12 | 11 | ineq2d 4173 |
. . . . . 6
β’ (π₯ = π΄ β (π΅ β© π« π₯) = (π΅ β© π« π΄)) |
13 | 12 | unieqd 4880 |
. . . . 5
β’ (π₯ = π΄ β βͺ (π΅ β© π« π₯) = βͺ
(π΅ β© π« π΄)) |
14 | 10, 13 | sseq12d 3978 |
. . . 4
β’ (π₯ = π΄ β (π₯ β βͺ (π΅ β© π« π₯) β π΄ β βͺ (π΅ β© π« π΄))) |
15 | 14 | elabg 3629 |
. . 3
β’ (π΄ β V β (π΄ β {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)} β π΄ β βͺ (π΅ β© π« π΄))) |
16 | 4, 9, 15 | pm5.21nd 801 |
. 2
β’ (π΅ β π β (π΄ β {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)} β π΄ β βͺ (π΅ β© π« π΄))) |
17 | 2, 16 | bitrd 279 |
1
β’ (π΅ β π β (π΄ β (topGenβπ΅) β π΄ β βͺ (π΅ β© π« π΄))) |