Step | Hyp | Ref
| Expression |
1 | | kgencmp 23056 |
. . 3
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β (π½ βΎt πΎ) = ((πGenβπ½) βΎt πΎ)) |
2 | | simpr 485 |
. . 3
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β (π½ βΎt πΎ) β Comp) |
3 | 1, 2 | eqeltrrd 2834 |
. 2
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β
((πGenβπ½)
βΎt πΎ)
β Comp) |
4 | | cmptop 22906 |
. . . . . . 7
β’
(((πGenβπ½) βΎt πΎ) β Comp β
((πGenβπ½)
βΎt πΎ)
β Top) |
5 | | restrcl 22668 |
. . . . . . . 8
β’
(((πGenβπ½) βΎt πΎ) β Top β
((πGenβπ½)
β V β§ πΎ β
V)) |
6 | 5 | simprd 496 |
. . . . . . 7
β’
(((πGenβπ½) βΎt πΎ) β Top β πΎ β V) |
7 | 4, 6 | syl 17 |
. . . . . 6
β’
(((πGenβπ½) βΎt πΎ) β Comp β πΎ β V) |
8 | | resttop 22671 |
. . . . . 6
β’ ((π½ β Top β§ πΎ β V) β (π½ βΎt πΎ) β Top) |
9 | 7, 8 | sylan2 593 |
. . . . 5
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (π½
βΎt πΎ)
β Top) |
10 | | toptopon2 22427 |
. . . . 5
β’ ((π½ βΎt πΎ) β Top β (π½ βΎt πΎ) β (TopOnββͺ (π½
βΎt πΎ))) |
11 | 9, 10 | sylib 217 |
. . . 4
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (π½
βΎt πΎ)
β (TopOnββͺ (π½ βΎt πΎ))) |
12 | | eqid 2732 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
13 | 12 | kgenuni 23050 |
. . . . . . . 8
β’ (π½ β Top β βͺ π½ =
βͺ (πGenβπ½)) |
14 | 13 | adantr 481 |
. . . . . . 7
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β βͺ π½ = βͺ
(πGenβπ½)) |
15 | 14 | ineq2d 4212 |
. . . . . 6
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (πΎ
β© βͺ π½) = (πΎ β© βͺ
(πGenβπ½))) |
16 | 12 | restuni2 22678 |
. . . . . . 7
β’ ((π½ β Top β§ πΎ β V) β (πΎ β© βͺ π½) =
βͺ (π½ βΎt πΎ)) |
17 | 7, 16 | sylan2 593 |
. . . . . 6
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (πΎ
β© βͺ π½) = βͺ (π½ βΎt πΎ)) |
18 | | kgenftop 23051 |
. . . . . . 7
β’ (π½ β Top β
(πGenβπ½)
β Top) |
19 | | eqid 2732 |
. . . . . . . 8
β’ βͺ (πGenβπ½) = βͺ
(πGenβπ½) |
20 | 19 | restuni2 22678 |
. . . . . . 7
β’
(((πGenβπ½) β Top β§ πΎ β V) β (πΎ β© βͺ
(πGenβπ½)) =
βͺ ((πGenβπ½) βΎt πΎ)) |
21 | 18, 7, 20 | syl2an 596 |
. . . . . 6
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (πΎ
β© βͺ (πGenβπ½)) = βͺ
((πGenβπ½)
βΎt πΎ)) |
22 | 15, 17, 21 | 3eqtr3d 2780 |
. . . . 5
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β βͺ (π½ βΎt πΎ) = βͺ
((πGenβπ½)
βΎt πΎ)) |
23 | 22 | fveq2d 6895 |
. . . 4
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (TopOnββͺ (π½ βΎt πΎ)) = (TopOnββͺ ((πGenβπ½) βΎt πΎ))) |
24 | 11, 23 | eleqtrd 2835 |
. . 3
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (π½
βΎt πΎ)
β (TopOnββͺ ((πGenβπ½) βΎt πΎ))) |
25 | | simpr 485 |
. . 3
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β ((πGenβπ½) βΎt πΎ) β Comp) |
26 | | kgenss 23054 |
. . . . 5
β’ (π½ β Top β π½ β
(πGenβπ½)) |
27 | 26 | adantr 481 |
. . . 4
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β π½
β (πGenβπ½)) |
28 | | ssrest 22687 |
. . . 4
β’
(((πGenβπ½) β Top β§ π½ β (πGenβπ½)) β (π½ βΎt πΎ) β ((πGenβπ½) βΎt πΎ)) |
29 | 18, 27, 28 | syl2an2r 683 |
. . 3
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (π½
βΎt πΎ)
β ((πGenβπ½) βΎt πΎ)) |
30 | | eqid 2732 |
. . . 4
β’ βͺ ((πGenβπ½) βΎt πΎ) = βͺ
((πGenβπ½)
βΎt πΎ) |
31 | 30 | sscmp 22916 |
. . 3
β’ (((π½ βΎt πΎ) β (TopOnββͺ ((πGenβπ½) βΎt πΎ)) β§ ((πGenβπ½) βΎt πΎ) β Comp β§ (π½ βΎt πΎ) β
((πGenβπ½)
βΎt πΎ))
β (π½
βΎt πΎ)
β Comp) |
32 | 24, 25, 29, 31 | syl3anc 1371 |
. 2
β’ ((π½ β Top β§
((πGenβπ½)
βΎt πΎ)
β Comp) β (π½
βΎt πΎ)
β Comp) |
33 | 3, 32 | impbida 799 |
1
β’ (π½ β Top β ((π½ βΎt πΎ) β Comp β
((πGenβπ½)
βΎt πΎ)
β Comp)) |