Step | Hyp | Ref
| Expression |
1 | | kgenftop 23044 |
. . . 4
β’ (π½ β Top β
(πGenβπ½)
β Top) |
2 | 1 | adantr 482 |
. . 3
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β
(πGenβπ½)
β Top) |
3 | | kgenss 23047 |
. . . 4
β’ (π½ β Top β π½ β
(πGenβπ½)) |
4 | 3 | adantr 482 |
. . 3
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β π½ β
(πGenβπ½)) |
5 | | ssrest 22680 |
. . 3
β’
(((πGenβπ½) β Top β§ π½ β (πGenβπ½)) β (π½ βΎt πΎ) β ((πGenβπ½) βΎt πΎ)) |
6 | 2, 4, 5 | syl2anc 585 |
. 2
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β (π½ βΎt πΎ) β
((πGenβπ½)
βΎt πΎ)) |
7 | | cmptop 22899 |
. . . . . 6
β’ ((π½ βΎt πΎ) β Comp β (π½ βΎt πΎ) β Top) |
8 | 7 | adantl 483 |
. . . . 5
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β (π½ βΎt πΎ) β Top) |
9 | | restrcl 22661 |
. . . . . 6
β’ ((π½ βΎt πΎ) β Top β (π½ β V β§ πΎ β V)) |
10 | 9 | simprd 497 |
. . . . 5
β’ ((π½ βΎt πΎ) β Top β πΎ β V) |
11 | 8, 10 | syl 17 |
. . . 4
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β πΎ β V) |
12 | | restval 17372 |
. . . 4
β’
(((πGenβπ½) β Top β§ πΎ β V) β ((πGenβπ½) βΎt πΎ) = ran (π₯ β (πGenβπ½) β¦ (π₯ β© πΎ))) |
13 | 2, 11, 12 | syl2anc 585 |
. . 3
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β
((πGenβπ½)
βΎt πΎ) =
ran (π₯ β
(πGenβπ½)
β¦ (π₯ β© πΎ))) |
14 | | simpr 486 |
. . . . . 6
β’ (((π½ β Top β§ (π½ βΎt πΎ) β Comp) β§ π₯ β
(πGenβπ½))
β π₯ β
(πGenβπ½)) |
15 | | simplr 768 |
. . . . . 6
β’ (((π½ β Top β§ (π½ βΎt πΎ) β Comp) β§ π₯ β
(πGenβπ½))
β (π½
βΎt πΎ)
β Comp) |
16 | | kgeni 23041 |
. . . . . 6
β’ ((π₯ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π₯
β© πΎ) β (π½ βΎt πΎ)) |
17 | 14, 15, 16 | syl2anc 585 |
. . . . 5
β’ (((π½ β Top β§ (π½ βΎt πΎ) β Comp) β§ π₯ β
(πGenβπ½))
β (π₯ β© πΎ) β (π½ βΎt πΎ)) |
18 | 17 | fmpttd 7115 |
. . . 4
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β (π₯ β
(πGenβπ½)
β¦ (π₯ β© πΎ)):(πGenβπ½)βΆ(π½ βΎt πΎ)) |
19 | 18 | frnd 6726 |
. . 3
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β ran (π₯ β
(πGenβπ½)
β¦ (π₯ β© πΎ)) β (π½ βΎt πΎ)) |
20 | 13, 19 | eqsstrd 4021 |
. 2
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β
((πGenβπ½)
βΎt πΎ)
β (π½
βΎt πΎ)) |
21 | 6, 20 | eqssd 4000 |
1
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β (π½ βΎt πΎ) = ((πGenβπ½) βΎt πΎ)) |