Step | Hyp | Ref
| Expression |
1 | | tgvalex 12711 |
. . . . 5
β’ (π΅ β π β (topGenβπ΅) β V) |
2 | | eltg3 13527 |
. . . . 5
β’
((topGenβπ΅)
β V β (π₯ β
(topGenβ(topGenβπ΅)) β βπ¦(π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦))) |
3 | 1, 2 | syl 14 |
. . . 4
β’ (π΅ β π β (π₯ β (topGenβ(topGenβπ΅)) β βπ¦(π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦))) |
4 | | uniiun 3940 |
. . . . . . . . . 10
β’ βͺ π¦ =
βͺ π§ β π¦ π§ |
5 | | simpr 110 |
. . . . . . . . . . . . 13
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β π¦ β (topGenβπ΅)) |
6 | 5 | sselda 3155 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π¦ β (topGenβπ΅)) β§ π§ β π¦) β π§ β (topGenβπ΅)) |
7 | | eltg4i 13525 |
. . . . . . . . . . . 12
β’ (π§ β (topGenβπ΅) β π§ = βͺ (π΅ β© π« π§)) |
8 | 6, 7 | syl 14 |
. . . . . . . . . . 11
β’ (((π΅ β π β§ π¦ β (topGenβπ΅)) β§ π§ β π¦) β π§ = βͺ (π΅ β© π« π§)) |
9 | 8 | iuneq2dv 3907 |
. . . . . . . . . 10
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π§ β π¦ π§ = βͺ π§ β π¦ βͺ (π΅ β© π« π§)) |
10 | 4, 9 | eqtrid 2222 |
. . . . . . . . 9
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π¦ = βͺ π§ β π¦ βͺ (π΅ β© π« π§)) |
11 | | iuncom4 3893 |
. . . . . . . . 9
β’ βͺ π§ β π¦ βͺ (π΅ β© π« π§) = βͺ
βͺ π§ β π¦ (π΅ β© π« π§) |
12 | 10, 11 | eqtrdi 2226 |
. . . . . . . 8
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π¦ = βͺ
βͺ π§ β π¦ (π΅ β© π« π§)) |
13 | | inss1 3355 |
. . . . . . . . . . . 12
β’ (π΅ β© π« π§) β π΅ |
14 | 13 | rgenw 2532 |
. . . . . . . . . . 11
β’
βπ§ β
π¦ (π΅ β© π« π§) β π΅ |
15 | | iunss 3927 |
. . . . . . . . . . 11
β’ (βͺ π§ β π¦ (π΅ β© π« π§) β π΅ β βπ§ β π¦ (π΅ β© π« π§) β π΅) |
16 | 14, 15 | mpbir 146 |
. . . . . . . . . 10
β’ βͺ π§ β π¦ (π΅ β© π« π§) β π΅ |
17 | 16 | a1i 9 |
. . . . . . . . 9
β’ (π¦ β (topGenβπ΅) β βͺ π§ β π¦ (π΅ β© π« π§) β π΅) |
18 | | eltg3i 13526 |
. . . . . . . . 9
β’ ((π΅ β π β§ βͺ
π§ β π¦ (π΅ β© π« π§) β π΅) β βͺ
βͺ π§ β π¦ (π΅ β© π« π§) β (topGenβπ΅)) |
19 | 17, 18 | sylan2 286 |
. . . . . . . 8
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ
βͺ π§ β π¦ (π΅ β© π« π§) β (topGenβπ΅)) |
20 | 12, 19 | eqeltrd 2254 |
. . . . . . 7
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β βͺ π¦ β (topGenβπ΅)) |
21 | | eleq1 2240 |
. . . . . . 7
β’ (π₯ = βͺ
π¦ β (π₯ β (topGenβπ΅) β βͺ π¦
β (topGenβπ΅))) |
22 | 20, 21 | syl5ibrcom 157 |
. . . . . 6
β’ ((π΅ β π β§ π¦ β (topGenβπ΅)) β (π₯ = βͺ π¦ β π₯ β (topGenβπ΅))) |
23 | 22 | expimpd 363 |
. . . . 5
β’ (π΅ β π β ((π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦) β π₯ β (topGenβπ΅))) |
24 | 23 | exlimdv 1819 |
. . . 4
β’ (π΅ β π β (βπ¦(π¦ β (topGenβπ΅) β§ π₯ = βͺ π¦) β π₯ β (topGenβπ΅))) |
25 | 3, 24 | sylbid 150 |
. . 3
β’ (π΅ β π β (π₯ β (topGenβ(topGenβπ΅)) β π₯ β (topGenβπ΅))) |
26 | 25 | ssrdv 3161 |
. 2
β’ (π΅ β π β (topGenβ(topGenβπ΅)) β (topGenβπ΅)) |
27 | | bastg 13531 |
. . 3
β’ (π΅ β π β π΅ β (topGenβπ΅)) |
28 | | tgss 13533 |
. . 3
β’
(((topGenβπ΅)
β V β§ π΅ β
(topGenβπ΅)) β
(topGenβπ΅) β
(topGenβ(topGenβπ΅))) |
29 | 1, 27, 28 | syl2anc 411 |
. 2
β’ (π΅ β π β (topGenβπ΅) β (topGenβ(topGenβπ΅))) |
30 | 26, 29 | eqssd 3172 |
1
β’ (π΅ β π β (topGenβ(topGenβπ΅)) = (topGenβπ΅)) |