Step | Hyp | Ref
| Expression |
1 | | df-lm 22953 |
. 2
β’
βπ‘ = (π β Top β¦ {β¨π, π₯β© β£ (π β (βͺ π βpm β)
β§ π₯ β βͺ π
β§ βπ’ β
π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |
2 | | simpr 483 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π = π½) β π = π½) |
3 | 2 | unieqd 4921 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π = π½) β βͺ π = βͺ
π½) |
4 | | toponuni 22636 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
5 | 4 | adantr 479 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π = π½) β π = βͺ π½) |
6 | 3, 5 | eqtr4d 2773 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π = π½) β βͺ π = π) |
7 | 6 | oveq1d 7426 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π = π½) β (βͺ π βpm β) =
(π βpm
β)) |
8 | 7 | eleq2d 2817 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (π β (βͺ π βpm β)
β π β (π βpm
β))) |
9 | 6 | eleq2d 2817 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (π₯ β βͺ π β π₯ β π)) |
10 | 2 | raleqdv 3323 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’) β βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))) |
11 | 8, 9, 10 | 3anbi123d 1434 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π = π½) β ((π β (βͺ π βpm β)
β§ π₯ β βͺ π
β§ βπ’ β
π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)) β (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)))) |
12 | 11 | opabbidv 5213 |
. 2
β’ ((π½ β (TopOnβπ) β§ π = π½) β {β¨π, π₯β© β£ (π β (βͺ π βpm β)
β§ π₯ β βͺ π
β§ βπ’ β
π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} = {β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |
13 | | topontop 22635 |
. 2
β’ (π½ β (TopOnβπ) β π½ β Top) |
14 | | df-3an 1087 |
. . . . 5
β’ ((π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)) β ((π β (π βpm β) β§ π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))) |
15 | 14 | opabbii 5214 |
. . . 4
β’
{β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} = {β¨π, π₯β© β£ ((π β (π βpm β) β§ π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} |
16 | | opabssxp 5767 |
. . . 4
β’
{β¨π, π₯β© β£ ((π β (π βpm β) β§ π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ π) |
17 | 15, 16 | eqsstri 4015 |
. . 3
β’
{β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ π) |
18 | | ovex 7444 |
. . . 4
β’ (π βpm β)
β V |
19 | | toponmax 22648 |
. . . 4
β’ (π½ β (TopOnβπ) β π β π½) |
20 | | xpexg 7739 |
. . . 4
β’ (((π βpm β)
β V β§ π β
π½) β ((π βpm β)
Γ π) β
V) |
21 | 18, 19, 20 | sylancr 585 |
. . 3
β’ (π½ β (TopOnβπ) β ((π βpm β) Γ π) β V) |
22 | | ssexg 5322 |
. . 3
β’
(({β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ π) β§ ((π βpm β) Γ π) β V) β {β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β V) |
23 | 17, 21, 22 | sylancr 585 |
. 2
β’ (π½ β (TopOnβπ) β {β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β V) |
24 | 1, 12, 13, 23 | fvmptd2 7005 |
1
β’ (π½ β (TopOnβπ) β
(βπ‘βπ½) = {β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |