Step | Hyp | Ref
| Expression |
1 | | prdstopn.y |
. . . . . 6
β’ π = (πXsπ
) |
2 | | prdstopn.s |
. . . . . 6
β’ (π β π β π) |
3 | | prdstopn.r |
. . . . . . 7
β’ (π β π
Fn πΌ) |
4 | | prdstopn.i |
. . . . . . 7
β’ (π β πΌ β π) |
5 | | fnex 7171 |
. . . . . . 7
β’ ((π
Fn πΌ β§ πΌ β π) β π
β V) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . 6
β’ (π β π
β V) |
7 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
8 | | eqidd 2734 |
. . . . . 6
β’ (π β dom π
= dom π
) |
9 | | eqid 2733 |
. . . . . 6
β’
(TopSetβπ) =
(TopSetβπ) |
10 | 1, 2, 6, 7, 8, 9 | prdstset 17356 |
. . . . 5
β’ (π β (TopSetβπ) =
(βtβ(TopOpen β π
))) |
11 | | topnfn 17315 |
. . . . . . . . . . 11
β’ TopOpen
Fn V |
12 | | dffn2 6674 |
. . . . . . . . . . . 12
β’ (π
Fn πΌ β π
:πΌβΆV) |
13 | 3, 12 | sylib 217 |
. . . . . . . . . . 11
β’ (π β π
:πΌβΆV) |
14 | | fnfco 6711 |
. . . . . . . . . . 11
β’ ((TopOpen
Fn V β§ π
:πΌβΆV) β (TopOpen
β π
) Fn πΌ) |
15 | 11, 13, 14 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (TopOpen β π
) Fn πΌ) |
16 | | eqid 2733 |
. . . . . . . . . . 11
β’ {π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} = {π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} |
17 | 16 | ptval 22944 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (TopOpen β π
) Fn πΌ) β (βtβ(TopOpen
β π
)) =
(topGenβ{π₯ β£
βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))})) |
18 | 4, 15, 17 | syl2anc 585 |
. . . . . . . . 9
β’ (π β
(βtβ(TopOpen β π
)) = (topGenβ{π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))})) |
19 | 18 | unieqd 4883 |
. . . . . . . 8
β’ (π β βͺ (βtβ(TopOpen β π
)) = βͺ (topGenβ{π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))})) |
20 | | fvco2 6942 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
Fn πΌ β§ π¦ β πΌ) β ((TopOpen β π
)βπ¦) = (TopOpenβ(π
βπ¦))) |
21 | 3, 20 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β πΌ) β ((TopOpen β π
)βπ¦) = (TopOpenβ(π
βπ¦))) |
22 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(Baseβ(π
βπ¦)) = (Baseβ(π
βπ¦)) |
23 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(TopSetβ(π
βπ¦)) = (TopSetβ(π
βπ¦)) |
24 | 22, 23 | topnval 17324 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((TopSetβ(π
βπ¦)) βΎt (Baseβ(π
βπ¦))) = (TopOpenβ(π
βπ¦)) |
25 | | restsspw 17321 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((TopSetβ(π
βπ¦)) βΎt (Baseβ(π
βπ¦))) β π« (Baseβ(π
βπ¦)) |
26 | 24, 25 | eqsstrri 3983 |
. . . . . . . . . . . . . . . . . . . 20
β’
(TopOpenβ(π
βπ¦)) β π« (Baseβ(π
βπ¦)) |
27 | 21, 26 | eqsstrdi 4002 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β πΌ) β ((TopOpen β π
)βπ¦) β π« (Baseβ(π
βπ¦))) |
28 | 27 | sseld 3947 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β πΌ) β ((πβπ¦) β ((TopOpen β π
)βπ¦) β (πβπ¦) β π« (Baseβ(π
βπ¦)))) |
29 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . 19
β’ (πβπ¦) β V |
30 | 29 | elpw 4568 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ¦) β π« (Baseβ(π
βπ¦)) β (πβπ¦) β (Baseβ(π
βπ¦))) |
31 | 28, 30 | syl6ib 251 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β πΌ) β ((πβπ¦) β ((TopOpen β π
)βπ¦) β (πβπ¦) β (Baseβ(π
βπ¦)))) |
32 | 31 | ralimdva 3161 |
. . . . . . . . . . . . . . . 16
β’ (π β (βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β βπ¦ β πΌ (πβπ¦) β (Baseβ(π
βπ¦)))) |
33 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
β’ (((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦)) β βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦)) |
34 | 32, 33 | impel 507 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))) β βπ¦ β πΌ (πβπ¦) β (Baseβ(π
βπ¦))) |
35 | | ss2ixp 8854 |
. . . . . . . . . . . . . . 15
β’
(βπ¦ β
πΌ (πβπ¦) β (Baseβ(π
βπ¦)) β Xπ¦ β πΌ (πβπ¦) β Xπ¦ β πΌ (Baseβ(π
βπ¦))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))) β Xπ¦ β πΌ (πβπ¦) β Xπ¦ β πΌ (Baseβ(π
βπ¦))) |
37 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))) β π₯ = Xπ¦ β πΌ (πβπ¦)) |
38 | 1, 7, 2, 4, 3 | prdsbas2 17359 |
. . . . . . . . . . . . . . 15
β’ (π β (Baseβπ) = Xπ¦ β
πΌ (Baseβ(π
βπ¦))) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))) β (Baseβπ) = Xπ¦ β πΌ (Baseβ(π
βπ¦))) |
40 | 36, 37, 39 | 3sstr4d 3995 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))) β π₯ β (Baseβπ)) |
41 | 40 | ex 414 |
. . . . . . . . . . . 12
β’ (π β (((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦)) β π₯ β (Baseβπ))) |
42 | 41 | exlimdv 1937 |
. . . . . . . . . . 11
β’ (π β (βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦)) β π₯ β (Baseβπ))) |
43 | | velpw 4569 |
. . . . . . . . . . 11
β’ (π₯ β π«
(Baseβπ) β π₯ β (Baseβπ)) |
44 | 42, 43 | syl6ibr 252 |
. . . . . . . . . 10
β’ (π β (βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦)) β π₯ β π« (Baseβπ))) |
45 | 44 | abssdv 4029 |
. . . . . . . . 9
β’ (π β {π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} β π« (Baseβπ)) |
46 | | fvex 6859 |
. . . . . . . . . . 11
β’
(Baseβπ)
β V |
47 | 46 | pwex 5339 |
. . . . . . . . . 10
β’ π«
(Baseβπ) β
V |
48 | 47 | ssex 5282 |
. . . . . . . . 9
β’ ({π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} β π« (Baseβπ) β {π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} β V) |
49 | | unitg 22340 |
. . . . . . . . 9
β’ ({π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} β V β βͺ (topGenβ{π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))}) = βͺ {π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))}) |
50 | 45, 48, 49 | 3syl 18 |
. . . . . . . 8
β’ (π β βͺ (topGenβ{π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))}) = βͺ {π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))}) |
51 | 19, 50 | eqtrd 2773 |
. . . . . . 7
β’ (π β βͺ (βtβ(TopOpen β π
)) = βͺ {π₯
β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))}) |
52 | | sspwuni 5064 |
. . . . . . . 8
β’ ({π₯ β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} β π« (Baseβπ) β βͺ {π₯
β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} β (Baseβπ)) |
53 | 45, 52 | sylib 217 |
. . . . . . 7
β’ (π β βͺ {π₯
β£ βπ((π Fn πΌ β§ βπ¦ β πΌ (πβπ¦) β ((TopOpen β π
)βπ¦) β§ βπ§ β Fin βπ¦ β (πΌ β π§)(πβπ¦) = βͺ ((TopOpen
β π
)βπ¦)) β§ π₯ = Xπ¦ β πΌ (πβπ¦))} β (Baseβπ)) |
54 | 51, 53 | eqsstrd 3986 |
. . . . . 6
β’ (π β βͺ (βtβ(TopOpen β π
)) β (Baseβπ)) |
55 | | sspwuni 5064 |
. . . . . 6
β’
((βtβ(TopOpen β π
)) β π« (Baseβπ) β βͺ (βtβ(TopOpen β π
)) β (Baseβπ)) |
56 | 54, 55 | sylibr 233 |
. . . . 5
β’ (π β
(βtβ(TopOpen β π
)) β π« (Baseβπ)) |
57 | 10, 56 | eqsstrd 3986 |
. . . 4
β’ (π β (TopSetβπ) β π«
(Baseβπ)) |
58 | 7, 9 | topnid 17325 |
. . . 4
β’
((TopSetβπ)
β π« (Baseβπ) β (TopSetβπ) = (TopOpenβπ)) |
59 | 57, 58 | syl 17 |
. . 3
β’ (π β (TopSetβπ) = (TopOpenβπ)) |
60 | | prdstopn.o |
. . 3
β’ π = (TopOpenβπ) |
61 | 59, 60 | eqtr4di 2791 |
. 2
β’ (π β (TopSetβπ) = π) |
62 | 61, 10 | eqtr3d 2775 |
1
β’ (π β π = (βtβ(TopOpen
β π
))) |