Step | Hyp | Ref
| Expression |
1 | | cmptop 22769 |
. . 3
β’ (π½ β Comp β π½ β Top) |
2 | | fitop 22272 |
. . . . 5
β’ (π½ β Top β
(fiβπ½) = π½) |
3 | 2 | fveq2d 6850 |
. . . 4
β’ (π½ β Top β
(topGenβ(fiβπ½))
= (topGenβπ½)) |
4 | | tgtop 22346 |
. . . 4
β’ (π½ β Top β
(topGenβπ½) = π½) |
5 | 3, 4 | eqtr2d 2774 |
. . 3
β’ (π½ β Top β π½ = (topGenβ(fiβπ½))) |
6 | 1, 5 | syl 17 |
. 2
β’ (π½ β Comp β π½ = (topGenβ(fiβπ½))) |
7 | | velpw 4569 |
. . . 4
β’ (π β π« π½ β π β π½) |
8 | | alexsubALT.1 |
. . . . . 6
β’ π = βͺ
π½ |
9 | 8 | cmpcov 22763 |
. . . . 5
β’ ((π½ β Comp β§ π β π½ β§ π = βͺ π) β βπ β (π« π β© Fin)π = βͺ π) |
10 | 9 | 3exp 1120 |
. . . 4
β’ (π½ β Comp β (π β π½ β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
11 | 7, 10 | biimtrid 241 |
. . 3
β’ (π½ β Comp β (π β π« π½ β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
12 | 11 | ralrimiv 3139 |
. 2
β’ (π½ β Comp β
βπ β π«
π½(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)) |
13 | | 2fveq3 6851 |
. . . . 5
β’ (π₯ = π½ β (topGenβ(fiβπ₯)) =
(topGenβ(fiβπ½))) |
14 | 13 | eqeq2d 2744 |
. . . 4
β’ (π₯ = π½ β (π½ = (topGenβ(fiβπ₯)) β π½ = (topGenβ(fiβπ½)))) |
15 | | pweq 4578 |
. . . . 5
β’ (π₯ = π½ β π« π₯ = π« π½) |
16 | 15 | raleqdv 3312 |
. . . 4
β’ (π₯ = π½ β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β βπ β π« π½(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
17 | 14, 16 | anbi12d 632 |
. . 3
β’ (π₯ = π½ β ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)) β (π½ = (topGenβ(fiβπ½)) β§ βπ β π« π½(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
18 | 17 | spcegv 3558 |
. 2
β’ (π½ β Comp β ((π½ = (topGenβ(fiβπ½)) β§ βπ β π« π½(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)) β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
19 | 6, 12, 18 | mp2and 698 |
1
β’ (π½ β Comp β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |