Step | Hyp | Ref
| Expression |
1 | | uniss 4878 |
. . . . . . 7
β’ (π₯ β
(πGenβπ½)
β βͺ π₯ β βͺ
(πGenβπ½)) |
2 | | kgenval 22902 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β
(πGenβπ½) =
{π₯ β π« π β£ βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π))}) |
3 | | ssrab2 4042 |
. . . . . . . . 9
β’ {π₯ β π« π β£ βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π))} β π« π |
4 | 2, 3 | eqsstrdi 4003 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β
(πGenβπ½)
β π« π) |
5 | | sspwuni 5065 |
. . . . . . . 8
β’
((πGenβπ½) β π« π β βͺ
(πGenβπ½)
β π) |
6 | 4, 5 | sylib 217 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β βͺ (πGenβπ½) β π) |
7 | 1, 6 | sylan9ssr 3963 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β βͺ π₯
β π) |
8 | | iunin2 5036 |
. . . . . . . . . 10
β’ βͺ π¦ β π₯ (π β© π¦) = (π β© βͺ
π¦ β π₯ π¦) |
9 | | uniiun 5023 |
. . . . . . . . . . 11
β’ βͺ π₯ =
βͺ π¦ β π₯ π¦ |
10 | 9 | ineq2i 4174 |
. . . . . . . . . 10
β’ (π β© βͺ π₯) =
(π β© βͺ π¦ β π₯ π¦) |
11 | | incom 4166 |
. . . . . . . . . 10
β’ (π β© βͺ π₯) =
(βͺ π₯ β© π) |
12 | 8, 10, 11 | 3eqtr2i 2771 |
. . . . . . . . 9
β’ βͺ π¦ β π₯ (π β© π¦) = (βͺ π₯ β© π) |
13 | | cmptop 22762 |
. . . . . . . . . . 11
β’ ((π½ βΎt π) β Comp β (π½ βΎt π) β Top) |
14 | 13 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π½ βΎt π) β Top) |
15 | | incom 4166 |
. . . . . . . . . . . 12
β’ (π¦ β© π) = (π β© π¦) |
16 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β π₯ β (πGenβπ½)) |
17 | 16 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β§ π¦ β π₯) β π¦ β (πGenβπ½)) |
18 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β§ π¦ β π₯) β (π½ βΎt π) β Comp) |
19 | | kgeni 22904 |
. . . . . . . . . . . . 13
β’ ((π¦ β
(πGenβπ½)
β§ (π½
βΎt π)
β Comp) β (π¦
β© π) β (π½ βΎt π)) |
20 | 17, 18, 19 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β§ π¦ β π₯) β (π¦ β© π) β (π½ βΎt π)) |
21 | 15, 20 | eqeltrrid 2843 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β§ π¦ β π₯) β (π β© π¦) β (π½ βΎt π)) |
22 | 21 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β βπ¦ β π₯ (π β© π¦) β (π½ βΎt π)) |
23 | | iunopn 22263 |
. . . . . . . . . 10
β’ (((π½ βΎt π) β Top β§ βπ¦ β π₯ (π β© π¦) β (π½ βΎt π)) β βͺ
π¦ β π₯ (π β© π¦) β (π½ βΎt π)) |
24 | 14, 22, 23 | syl2anc 585 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β βͺ π¦ β π₯ (π β© π¦) β (π½ βΎt π)) |
25 | 12, 24 | eqeltrrid 2843 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (βͺ π₯
β© π) β (π½ βΎt π)) |
26 | 25 | expr 458 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β§ π β π« π) β ((π½ βΎt π) β Comp β (βͺ π₯
β© π) β (π½ βΎt π))) |
27 | 26 | ralrimiva 3144 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β βπ β π« π((π½ βΎt π) β Comp β (βͺ π₯
β© π) β (π½ βΎt π))) |
28 | | elkgen 22903 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β (βͺ π₯
β (πGenβπ½) β (βͺ π₯ β π β§ βπ β π« π((π½ βΎt π) β Comp β (βͺ π₯
β© π) β (π½ βΎt π))))) |
29 | 28 | adantr 482 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β (βͺ π₯
β (πGenβπ½) β (βͺ π₯ β π β§ βπ β π« π((π½ βΎt π) β Comp β (βͺ π₯
β© π) β (π½ βΎt π))))) |
30 | 7, 27, 29 | mpbir2and 712 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π₯ β (πGenβπ½)) β βͺ π₯
β (πGenβπ½)) |
31 | 30 | ex 414 |
. . . 4
β’ (π½ β (TopOnβπ) β (π₯ β (πGenβπ½) β βͺ π₯
β (πGenβπ½))) |
32 | 31 | alrimiv 1931 |
. . 3
β’ (π½ β (TopOnβπ) β βπ₯(π₯ β (πGenβπ½) β βͺ π₯
β (πGenβπ½))) |
33 | | inss1 4193 |
. . . . . 6
β’ (π₯ β© π¦) β π₯ |
34 | | elssuni 4903 |
. . . . . . . 8
β’ (π₯ β
(πGenβπ½)
β π₯ β βͺ (πGenβπ½)) |
35 | 34 | ad2antrl 727 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β π₯ β βͺ
(πGenβπ½)) |
36 | | ssidd 3972 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π β π) |
37 | | elpwi 4572 |
. . . . . . . . . . . . . . . 16
β’ (π β π« π β π β π) |
38 | 37 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β π β π) |
39 | | sseqin2 4180 |
. . . . . . . . . . . . . . 15
β’ (π β π β (π β© π) = π) |
40 | 38, 39 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π½ β (TopOnβπ) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π β© π) = π) |
41 | 37 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β π« π β§ (π½ βΎt π) β Comp) β π β π) |
42 | | resttopon 22528 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ π β π) β (π½ βΎt π) β (TopOnβπ)) |
43 | 41, 42 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π½ βΎt π) β (TopOnβπ)) |
44 | | toponmax 22291 |
. . . . . . . . . . . . . . 15
β’ ((π½ βΎt π) β (TopOnβπ) β π β (π½ βΎt π)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π½ β (TopOnβπ) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β π β (π½ βΎt π)) |
46 | 40, 45 | eqeltrd 2838 |
. . . . . . . . . . . . 13
β’ ((π½ β (TopOnβπ) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π β© π) β (π½ βΎt π)) |
47 | 46 | expr 458 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπ) β§ π β π« π) β ((π½ βΎt π) β Comp β (π β© π) β (π½ βΎt π))) |
48 | 47 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β βπ β π« π((π½ βΎt π) β Comp β (π β© π) β (π½ βΎt π))) |
49 | | elkgen 22903 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β (π β (πGenβπ½) β (π β π β§ βπ β π« π((π½ βΎt π) β Comp β (π β© π) β (π½ βΎt π))))) |
50 | 36, 48, 49 | mpbir2and 712 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π β (πGenβπ½)) |
51 | | elssuni 4903 |
. . . . . . . . . 10
β’ (π β
(πGenβπ½)
β π β βͺ (πGenβπ½)) |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π β βͺ
(πGenβπ½)) |
53 | 52, 6 | eqssd 3966 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π = βͺ
(πGenβπ½)) |
54 | 53 | adantr 482 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β π = βͺ
(πGenβπ½)) |
55 | 35, 54 | sseqtrrd 3990 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β π₯ β π) |
56 | 33, 55 | sstrid 3960 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β (π₯ β© π¦) β π) |
57 | | inindir 4192 |
. . . . . . . 8
β’ ((π₯ β© π¦) β© π) = ((π₯ β© π) β© (π¦ β© π)) |
58 | 13 | ad2antll 728 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π½ βΎt π) β Top) |
59 | | simplrl 776 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β π₯ β (πGenβπ½)) |
60 | | simprr 772 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π½ βΎt π) β Comp) |
61 | | kgeni 22904 |
. . . . . . . . . 10
β’ ((π₯ β
(πGenβπ½)
β§ (π½
βΎt π)
β Comp) β (π₯
β© π) β (π½ βΎt π)) |
62 | 59, 60, 61 | syl2anc 585 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π₯ β© π) β (π½ βΎt π)) |
63 | | simplrr 777 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β π¦ β (πGenβπ½)) |
64 | 63, 60, 19 | syl2anc 585 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β (π¦ β© π) β (π½ βΎt π)) |
65 | | inopn 22264 |
. . . . . . . . 9
β’ (((π½ βΎt π) β Top β§ (π₯ β© π) β (π½ βΎt π) β§ (π¦ β© π) β (π½ βΎt π)) β ((π₯ β© π) β© (π¦ β© π)) β (π½ βΎt π)) |
66 | 58, 62, 64, 65 | syl3anc 1372 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β ((π₯ β© π) β© (π¦ β© π)) β (π½ βΎt π)) |
67 | 57, 66 | eqeltrid 2842 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ (π β π« π β§ (π½ βΎt π) β Comp)) β ((π₯ β© π¦) β© π) β (π½ βΎt π)) |
68 | 67 | expr 458 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β§ π β π« π) β ((π½ βΎt π) β Comp β ((π₯ β© π¦) β© π) β (π½ βΎt π))) |
69 | 68 | ralrimiva 3144 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β βπ β π« π((π½ βΎt π) β Comp β ((π₯ β© π¦) β© π) β (π½ βΎt π))) |
70 | | elkgen 22903 |
. . . . . 6
β’ (π½ β (TopOnβπ) β ((π₯ β© π¦) β (πGenβπ½) β ((π₯ β© π¦) β π β§ βπ β π« π((π½ βΎt π) β Comp β ((π₯ β© π¦) β© π) β (π½ βΎt π))))) |
71 | 70 | adantr 482 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β ((π₯ β© π¦) β (πGenβπ½) β ((π₯ β© π¦) β π β§ βπ β π« π((π½ βΎt π) β Comp β ((π₯ β© π¦) β© π) β (π½ βΎt π))))) |
72 | 56, 69, 71 | mpbir2and 712 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (π₯ β (πGenβπ½) β§ π¦ β (πGenβπ½))) β (π₯ β© π¦) β (πGenβπ½)) |
73 | 72 | ralrimivva 3198 |
. . 3
β’ (π½ β (TopOnβπ) β βπ₯ β
(πGenβπ½)βπ¦ β (πGenβπ½)(π₯ β© π¦) β (πGenβπ½)) |
74 | | fvex 6860 |
. . . 4
β’
(πGenβπ½) β V |
75 | | istopg 22260 |
. . . 4
β’
((πGenβπ½) β V β ((πGenβπ½) β Top β
(βπ₯(π₯ β
(πGenβπ½)
β βͺ π₯ β (πGenβπ½)) β§ βπ₯ β (πGenβπ½)βπ¦ β (πGenβπ½)(π₯ β© π¦) β (πGenβπ½)))) |
76 | 74, 75 | ax-mp 5 |
. . 3
β’
((πGenβπ½) β Top β (βπ₯(π₯ β (πGenβπ½) β βͺ π₯
β (πGenβπ½)) β§ βπ₯ β (πGenβπ½)βπ¦ β (πGenβπ½)(π₯ β© π¦) β (πGenβπ½))) |
77 | 32, 73, 76 | sylanbrc 584 |
. 2
β’ (π½ β (TopOnβπ) β
(πGenβπ½)
β Top) |
78 | | istopon 22277 |
. 2
β’
((πGenβπ½) β (TopOnβπ) β ((πGenβπ½) β Top β§ π = βͺ
(πGenβπ½))) |
79 | 77, 53, 78 | sylanbrc 584 |
1
β’ (π½ β (TopOnβπ) β
(πGenβπ½)
β (TopOnβπ)) |