Step | Hyp | Ref
| Expression |
1 | | topontop 22415 |
. . . . . . 7
β’ (π β (TopOnβπ) β π β Top) |
2 | 1 | ad2antrl 727 |
. . . . . 6
β’ (((π β π β§ π β (TopOnβπ)) β§ (π β (TopOnβπ) β§ βπ β π π β π)) β π β Top) |
3 | | toponmax 22428 |
. . . . . . . . 9
β’ (π β (TopOnβπ) β π β π) |
4 | 3 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β π β§ π β (TopOnβπ)) β§ (π β (TopOnβπ) β§ βπ β π π β π)) β π β π) |
5 | 4 | snssd 4813 |
. . . . . . 7
β’ (((π β π β§ π β (TopOnβπ)) β§ (π β (TopOnβπ) β§ βπ β π π β π)) β {π} β π) |
6 | | simprr 772 |
. . . . . . . 8
β’ (((π β π β§ π β (TopOnβπ)) β§ (π β (TopOnβπ) β§ βπ β π π β π)) β βπ β π π β π) |
7 | | unissb 4944 |
. . . . . . . 8
β’ (βͺ π
β π β
βπ β π π β π) |
8 | 6, 7 | sylibr 233 |
. . . . . . 7
β’ (((π β π β§ π β (TopOnβπ)) β§ (π β (TopOnβπ) β§ βπ β π π β π)) β βͺ π β π) |
9 | 5, 8 | unssd 4187 |
. . . . . 6
β’ (((π β π β§ π β (TopOnβπ)) β§ (π β (TopOnβπ) β§ βπ β π π β π)) β ({π} βͺ βͺ π) β π) |
10 | | tgfiss 22494 |
. . . . . 6
β’ ((π β Top β§ ({π} βͺ βͺ π)
β π) β
(topGenβ(fiβ({π} βͺ βͺ π))) β π) |
11 | 2, 9, 10 | syl2anc 585 |
. . . . 5
β’ (((π β π β§ π β (TopOnβπ)) β§ (π β (TopOnβπ) β§ βπ β π π β π)) β (topGenβ(fiβ({π} βͺ βͺ π)))
β π) |
12 | 11 | expr 458 |
. . . 4
β’ (((π β π β§ π β (TopOnβπ)) β§ π β (TopOnβπ)) β (βπ β π π β π β (topGenβ(fiβ({π} βͺ βͺ π)))
β π)) |
13 | 12 | ralrimiva 3147 |
. . 3
β’ ((π β π β§ π β (TopOnβπ)) β βπ β (TopOnβπ)(βπ β π π β π β (topGenβ(fiβ({π} βͺ βͺ π)))
β π)) |
14 | | ssintrab 4976 |
. . 3
β’
((topGenβ(fiβ({π} βͺ βͺ π))) β β© {π
β (TopOnβπ)
β£ βπ β
π π β π} β βπ β (TopOnβπ)(βπ β π π β π β (topGenβ(fiβ({π} βͺ βͺ π)))
β π)) |
15 | 13, 14 | sylibr 233 |
. 2
β’ ((π β π β§ π β (TopOnβπ)) β (topGenβ(fiβ({π} βͺ βͺ π)))
β β© {π β (TopOnβπ) β£ βπ β π π β π}) |
16 | | fibas 22480 |
. . . . . 6
β’
(fiβ({π} βͺ
βͺ π)) β TopBases |
17 | | tgtopon 22474 |
. . . . . 6
β’
((fiβ({π}
βͺ βͺ π)) β TopBases β
(topGenβ(fiβ({π} βͺ βͺ π))) β (TopOnββͺ (fiβ({π} βͺ βͺ π)))) |
18 | 16, 17 | ax-mp 5 |
. . . . 5
β’
(topGenβ(fiβ({π} βͺ βͺ π))) β (TopOnββͺ (fiβ({π} βͺ βͺ π))) |
19 | | uniun 4935 |
. . . . . . . 8
β’ βͺ ({π}
βͺ βͺ π) = (βͺ {π} βͺ βͺ βͺ π) |
20 | | unisng 4930 |
. . . . . . . . . 10
β’ (π β π β βͺ {π} = π) |
21 | 20 | adantr 482 |
. . . . . . . . 9
β’ ((π β π β§ π β (TopOnβπ)) β βͺ
{π} = π) |
22 | 21 | uneq1d 4163 |
. . . . . . . 8
β’ ((π β π β§ π β (TopOnβπ)) β (βͺ
{π} βͺ βͺ βͺ π) = (π βͺ βͺ βͺ π)) |
23 | 19, 22 | eqtr2id 2786 |
. . . . . . 7
β’ ((π β π β§ π β (TopOnβπ)) β (π βͺ βͺ βͺ π) =
βͺ ({π} βͺ βͺ π)) |
24 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (TopOnβπ)) β π β (TopOnβπ)) |
25 | | toponuni 22416 |
. . . . . . . . . . . . . . 15
β’ (π β (TopOnβπ) β π = βͺ π) |
26 | | eqimss2 4042 |
. . . . . . . . . . . . . . 15
β’ (π = βͺ
π β βͺ π
β π) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (TopOnβπ) β βͺ π
β π) |
28 | | sspwuni 5104 |
. . . . . . . . . . . . . 14
β’ (π β π« π β βͺ π
β π) |
29 | 27, 28 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π β (TopOnβπ) β π β π« π) |
30 | | velpw 4608 |
. . . . . . . . . . . . 13
β’ (π β π« π«
π β π β π« π) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . . . 12
β’ (π β (TopOnβπ) β π β π« π« π) |
32 | 31 | ssriv 3987 |
. . . . . . . . . . 11
β’
(TopOnβπ)
β π« π« π |
33 | 24, 32 | sstrdi 3995 |
. . . . . . . . . 10
β’ ((π β π β§ π β (TopOnβπ)) β π β π« π« π) |
34 | | sspwuni 5104 |
. . . . . . . . . 10
β’ (π β π« π«
π β βͺ π
β π« π) |
35 | 33, 34 | sylib 217 |
. . . . . . . . 9
β’ ((π β π β§ π β (TopOnβπ)) β βͺ π β π« π) |
36 | | sspwuni 5104 |
. . . . . . . . 9
β’ (βͺ π
β π« π β
βͺ βͺ π β π) |
37 | 35, 36 | sylib 217 |
. . . . . . . 8
β’ ((π β π β§ π β (TopOnβπ)) β βͺ βͺ π
β π) |
38 | | ssequn2 4184 |
. . . . . . . 8
β’ (βͺ βͺ π β π β (π βͺ βͺ βͺ π) =
π) |
39 | 37, 38 | sylib 217 |
. . . . . . 7
β’ ((π β π β§ π β (TopOnβπ)) β (π βͺ βͺ βͺ π) =
π) |
40 | | snex 5432 |
. . . . . . . . 9
β’ {π} β V |
41 | | fvex 6905 |
. . . . . . . . . . . 12
β’
(TopOnβπ)
β V |
42 | 41 | ssex 5322 |
. . . . . . . . . . 11
β’ (π β (TopOnβπ) β π β V) |
43 | 42 | adantl 483 |
. . . . . . . . . 10
β’ ((π β π β§ π β (TopOnβπ)) β π β V) |
44 | 43 | uniexd 7732 |
. . . . . . . . 9
β’ ((π β π β§ π β (TopOnβπ)) β βͺ π β V) |
45 | | unexg 7736 |
. . . . . . . . 9
β’ (({π} β V β§ βͺ π
β V) β ({π} βͺ
βͺ π) β V) |
46 | 40, 44, 45 | sylancr 588 |
. . . . . . . 8
β’ ((π β π β§ π β (TopOnβπ)) β ({π} βͺ βͺ π) β V) |
47 | | fiuni 9423 |
. . . . . . . 8
β’ (({π} βͺ βͺ π)
β V β βͺ ({π} βͺ βͺ π) = βͺ
(fiβ({π} βͺ βͺ π))) |
48 | 46, 47 | syl 17 |
. . . . . . 7
β’ ((π β π β§ π β (TopOnβπ)) β βͺ
({π} βͺ βͺ π) =
βͺ (fiβ({π} βͺ βͺ π))) |
49 | 23, 39, 48 | 3eqtr3d 2781 |
. . . . . 6
β’ ((π β π β§ π β (TopOnβπ)) β π = βͺ
(fiβ({π} βͺ βͺ π))) |
50 | 49 | fveq2d 6896 |
. . . . 5
β’ ((π β π β§ π β (TopOnβπ)) β (TopOnβπ) = (TopOnββͺ (fiβ({π} βͺ βͺ π)))) |
51 | 18, 50 | eleqtrrid 2841 |
. . . 4
β’ ((π β π β§ π β (TopOnβπ)) β (topGenβ(fiβ({π} βͺ βͺ π)))
β (TopOnβπ)) |
52 | | elssuni 4942 |
. . . . . . . 8
β’ (π β π β π β βͺ π) |
53 | | ssun2 4174 |
. . . . . . . 8
β’ βͺ π
β ({π} βͺ βͺ π) |
54 | 52, 53 | sstrdi 3995 |
. . . . . . 7
β’ (π β π β π β ({π} βͺ βͺ π)) |
55 | | ssfii 9414 |
. . . . . . . 8
β’ (({π} βͺ βͺ π)
β V β ({π} βͺ
βͺ π) β (fiβ({π} βͺ βͺ π))) |
56 | 46, 55 | syl 17 |
. . . . . . 7
β’ ((π β π β§ π β (TopOnβπ)) β ({π} βͺ βͺ π) β (fiβ({π} βͺ βͺ π))) |
57 | 54, 56 | sylan9ssr 3997 |
. . . . . 6
β’ (((π β π β§ π β (TopOnβπ)) β§ π β π) β π β (fiβ({π} βͺ βͺ π))) |
58 | | bastg 22469 |
. . . . . . 7
β’
((fiβ({π}
βͺ βͺ π)) β TopBases β (fiβ({π} βͺ βͺ π))
β (topGenβ(fiβ({π} βͺ βͺ π)))) |
59 | 16, 58 | ax-mp 5 |
. . . . . 6
β’
(fiβ({π} βͺ
βͺ π)) β (topGenβ(fiβ({π} βͺ βͺ π))) |
60 | 57, 59 | sstrdi 3995 |
. . . . 5
β’ (((π β π β§ π β (TopOnβπ)) β§ π β π) β π β (topGenβ(fiβ({π} βͺ βͺ π)))) |
61 | 60 | ralrimiva 3147 |
. . . 4
β’ ((π β π β§ π β (TopOnβπ)) β βπ β π π β (topGenβ(fiβ({π} βͺ βͺ π)))) |
62 | | sseq2 4009 |
. . . . . 6
β’ (π =
(topGenβ(fiβ({π} βͺ βͺ π))) β (π β π β π β (topGenβ(fiβ({π} βͺ βͺ π))))) |
63 | 62 | ralbidv 3178 |
. . . . 5
β’ (π =
(topGenβ(fiβ({π} βͺ βͺ π))) β (βπ β π π β π β βπ β π π β (topGenβ(fiβ({π} βͺ βͺ π))))) |
64 | 63 | elrab 3684 |
. . . 4
β’
((topGenβ(fiβ({π} βͺ βͺ π))) β {π β (TopOnβπ) β£ βπ β π π β π} β ((topGenβ(fiβ({π} βͺ βͺ π)))
β (TopOnβπ)
β§ βπ β
π π β (topGenβ(fiβ({π} βͺ βͺ π))))) |
65 | 51, 61, 64 | sylanbrc 584 |
. . 3
β’ ((π β π β§ π β (TopOnβπ)) β (topGenβ(fiβ({π} βͺ βͺ π)))
β {π β
(TopOnβπ) β£
βπ β π π β π}) |
66 | | intss1 4968 |
. . 3
β’
((topGenβ(fiβ({π} βͺ βͺ π))) β {π β (TopOnβπ) β£ βπ β π π β π} β β© {π β (TopOnβπ) β£ βπ β π π β π} β (topGenβ(fiβ({π} βͺ βͺ π)))) |
67 | 65, 66 | syl 17 |
. 2
β’ ((π β π β§ π β (TopOnβπ)) β β©
{π β
(TopOnβπ) β£
βπ β π π β π} β (topGenβ(fiβ({π} βͺ βͺ π)))) |
68 | 15, 67 | eqssd 4000 |
1
β’ ((π β π β§ π β (TopOnβπ)) β (topGenβ(fiβ({π} βͺ βͺ π)))
= β© {π β (TopOnβπ) β£ βπ β π π β π}) |