Step | Hyp | Ref
| Expression |
1 | | is2ndc 22820 |
. . 3
β’ (π½ β 2ndΟ
β βπ₯ β
TopBases (π₯ βΌ Ο
β§ (topGenβπ₯) =
π½)) |
2 | | simplr 768 |
. . . . . . . 8
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β π₯ β TopBases) |
3 | | simpll 766 |
. . . . . . . 8
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β π΄ β π) |
4 | | tgrest 22533 |
. . . . . . . 8
β’ ((π₯ β TopBases β§ π΄ β π) β (topGenβ(π₯ βΎt π΄)) = ((topGenβπ₯) βΎt π΄)) |
5 | 2, 3, 4 | syl2anc 585 |
. . . . . . 7
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β (topGenβ(π₯ βΎt π΄)) = ((topGenβπ₯) βΎt π΄)) |
6 | | restbas 22532 |
. . . . . . . . 9
β’ (π₯ β TopBases β (π₯ βΎt π΄) β
TopBases) |
7 | 6 | ad2antlr 726 |
. . . . . . . 8
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β (π₯ βΎt π΄) β TopBases) |
8 | | restval 17316 |
. . . . . . . . . 10
β’ ((π₯ β TopBases β§ π΄ β π) β (π₯ βΎt π΄) = ran (π¦ β π₯ β¦ (π¦ β© π΄))) |
9 | 2, 3, 8 | syl2anc 585 |
. . . . . . . . 9
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β (π₯ βΎt π΄) = ran (π¦ β π₯ β¦ (π¦ β© π΄))) |
10 | | 1stcrestlem 22826 |
. . . . . . . . . 10
β’ (π₯ βΌ Ο β ran
(π¦ β π₯ β¦ (π¦ β© π΄)) βΌ Ο) |
11 | 10 | adantl 483 |
. . . . . . . . 9
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β ran (π¦ β π₯ β¦ (π¦ β© π΄)) βΌ Ο) |
12 | 9, 11 | eqbrtrd 5131 |
. . . . . . . 8
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β (π₯ βΎt π΄) βΌ Ο) |
13 | | 2ndci 22822 |
. . . . . . . 8
β’ (((π₯ βΎt π΄) β TopBases β§ (π₯ βΎt π΄) βΌ Ο) β
(topGenβ(π₯
βΎt π΄))
β 2ndΟ) |
14 | 7, 12, 13 | syl2anc 585 |
. . . . . . 7
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β (topGenβ(π₯ βΎt π΄)) β
2ndΟ) |
15 | 5, 14 | eqeltrrd 2835 |
. . . . . 6
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β ((topGenβπ₯) βΎt π΄) β
2ndΟ) |
16 | | oveq1 7368 |
. . . . . . 7
β’
((topGenβπ₯) =
π½ β
((topGenβπ₯)
βΎt π΄) =
(π½ βΎt
π΄)) |
17 | 16 | eleq1d 2819 |
. . . . . 6
β’
((topGenβπ₯) =
π½ β
(((topGenβπ₯)
βΎt π΄)
β 2ndΟ β (π½ βΎt π΄) β
2ndΟ)) |
18 | 15, 17 | syl5ibcom 244 |
. . . . 5
β’ (((π΄ β π β§ π₯ β TopBases) β§ π₯ βΌ Ο) β ((topGenβπ₯) = π½ β (π½ βΎt π΄) β
2ndΟ)) |
19 | 18 | expimpd 455 |
. . . 4
β’ ((π΄ β π β§ π₯ β TopBases) β ((π₯ βΌ Ο β§ (topGenβπ₯) = π½) β (π½ βΎt π΄) β
2ndΟ)) |
20 | 19 | rexlimdva 3149 |
. . 3
β’ (π΄ β π β (βπ₯ β TopBases (π₯ βΌ Ο β§ (topGenβπ₯) = π½) β (π½ βΎt π΄) β
2ndΟ)) |
21 | 1, 20 | biimtrid 241 |
. 2
β’ (π΄ β π β (π½ β 2ndΟ β (π½ βΎt π΄) β
2ndΟ)) |
22 | 21 | impcom 409 |
1
β’ ((π½ β 2ndΟ
β§ π΄ β π) β (π½ βΎt π΄) β
2ndΟ) |