Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . 5
β’
(topGenβπ΅)
β V |
2 | | eltg3 22328 |
. . . . 5
β’
((topGenβπ΅)
β V β (π₯ β
(topGenβ(topGenβπ΅)) β βπ¦(π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦))) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ (π₯ β
(topGenβ(topGenβπ΅)) β βπ¦(π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦)) |
4 | | uniiun 5019 |
. . . . . . . . . 10
β’ βͺ π¦ =
βͺ π§ β π¦ π§ |
5 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β π¦ β (topGenβπ΅)) |
6 | 5 | sselda 3945 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π¦ β (topGenβπ΅)) β§ π§ β π¦) β π§ β (topGenβπ΅)) |
7 | | eltg4i 22326 |
. . . . . . . . . . . 12
β’ (π§ β (topGenβπ΅) β π§ = βͺ (π΅ β© π« π§)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
β’ (((π΅ β π β§ π¦ β (topGenβπ΅)) β§ π§ β π¦) β π§ = βͺ (π΅ β© π« π§)) |
9 | 8 | iuneq2dv 4979 |
. . . . . . . . . 10
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π§ β π¦ π§ = βͺ π§ β π¦ βͺ (π΅ β© π« π§)) |
10 | 4, 9 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π¦ = βͺ π§ β π¦ βͺ (π΅ β© π« π§)) |
11 | | iuncom4 4963 |
. . . . . . . . 9
β’ βͺ π§ β π¦ βͺ (π΅ β© π« π§) = βͺ
βͺ π§ β π¦ (π΅ β© π« π§) |
12 | 10, 11 | eqtrdi 2789 |
. . . . . . . 8
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π¦ = βͺ
βͺ π§ β π¦ (π΅ β© π« π§)) |
13 | | inss1 4189 |
. . . . . . . . . . . 12
β’ (π΅ β© π« π§) β π΅ |
14 | 13 | rgenw 3065 |
. . . . . . . . . . 11
β’
βπ§ β
π¦ (π΅ β© π« π§) β π΅ |
15 | | iunss 5006 |
. . . . . . . . . . 11
β’ (βͺ π§ β π¦ (π΅ β© π« π§) β π΅ β βπ§ β π¦ (π΅ β© π« π§) β π΅) |
16 | 14, 15 | mpbir 230 |
. . . . . . . . . 10
β’ βͺ π§ β π¦ (π΅ β© π« π§) β π΅ |
17 | 16 | a1i 11 |
. . . . . . . . 9
β’ (π¦ β (topGenβπ΅) β βͺ π§ β π¦ (π΅ β© π« π§) β π΅) |
18 | | eltg3i 22327 |
. . . . . . . . 9
β’ ((π΅ β π β§ βͺ
π§ β π¦ (π΅ β© π« π§) β π΅) β βͺ
βͺ π§ β π¦ (π΅ β© π« π§) β (topGenβπ΅)) |
19 | 17, 18 | sylan2 594 |
. . . . . . . 8
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ
βͺ π§ β π¦ (π΅ β© π« π§) β (topGenβπ΅)) |
20 | 12, 19 | eqeltrd 2834 |
. . . . . . 7
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π¦ β (topGenβπ΅)) |
21 | | eleq1 2822 |
. . . . . . 7
β’ (π₯ = βͺ
π¦ β (π₯ β (topGenβπ΅) β βͺ π¦
β (topGenβπ΅))) |
22 | 20, 21 | syl5ibrcom 247 |
. . . . . 6
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β (π₯ = βͺ π¦ β π₯ β (topGenβπ΅))) |
23 | 22 | expimpd 455 |
. . . . 5
β’ (π΅ β π β ((π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦) β π₯ β (topGenβπ΅))) |
24 | 23 | exlimdv 1937 |
. . . 4
β’ (π΅ β π β (βπ¦(π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦) β π₯ β (topGenβπ΅))) |
25 | 3, 24 | biimtrid 241 |
. . 3
β’ (π΅ β π β (π₯ β (topGenβ(topGenβπ΅)) β π₯ β (topGenβπ΅))) |
26 | 25 | ssrdv 3951 |
. 2
β’ (π΅ β π β (topGenβ(topGenβπ΅)) β (topGenβπ΅)) |
27 | | bastg 22332 |
. . 3
β’ (π΅ β π β π΅ β (topGenβπ΅)) |
28 | | tgss 22334 |
. . 3
β’
(((topGenβπ΅)
β V β§ π΅ β
(topGenβπ΅)) β
(topGenβπ΅) β
(topGenβ(topGenβπ΅))) |
29 | 1, 27, 28 | sylancr 588 |
. 2
β’ (π΅ β π β (topGenβπ΅) β (topGenβ(topGenβπ΅))) |
30 | 26, 29 | eqssd 3962 |
1
β’ (π΅ β π β (topGenβ(topGenβπ΅)) = (topGenβπ΅)) |