Step | Hyp | Ref
| Expression |
1 | | df-lm 13660 |
. . 3
β’
βπ‘ = (π β Top β¦ {β¨π, π₯β© β£ (π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |
2 | 1 | a1i 9 |
. 2
β’ (π½ β (TopOnβπ) β
βπ‘ = (π β Top β¦ {β¨π, π₯β© β£ (π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))})) |
3 | | simpr 110 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π = π½) β π = π½) |
4 | 3 | unieqd 3820 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π = π½) β βͺ π = βͺ
π½) |
5 | | toponuni 13485 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
6 | 5 | adantr 276 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π = π½) β π = βͺ π½) |
7 | 4, 6 | eqtr4d 2213 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π = π½) β βͺ π = π) |
8 | 7 | oveq1d 5889 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π = π½) β (βͺ π βpm
β) = (π
βpm β)) |
9 | 8 | eleq2d 2247 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (π β (βͺ π βpm
β) β π β
(π
βpm β))) |
10 | 7 | eleq2d 2247 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (π₯ β βͺ π β π₯ β π)) |
11 | 3 | raleqdv 2678 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’) β βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))) |
12 | 9, 10, 11 | 3anbi123d 1312 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π = π½) β ((π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)) β (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)))) |
13 | 12 | opabbidv 4069 |
. 2
β’ ((π½ β (TopOnβπ) β§ π = π½) β {β¨π, π₯β© β£ (π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} = {β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |
14 | | topontop 13484 |
. 2
β’ (π½ β (TopOnβπ) β π½ β Top) |
15 | | df-3an 980 |
. . . . 5
β’ ((π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)) β ((π β (π βpm β) β§
π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))) |
16 | 15 | opabbii 4070 |
. . . 4
β’
{β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} = {β¨π, π₯β© β£ ((π β (π βpm β) β§
π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} |
17 | | opabssxp 4700 |
. . . 4
β’
{β¨π, π₯β© β£ ((π β (π βpm β) β§
π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ
π) |
18 | 16, 17 | eqsstri 3187 |
. . 3
β’
{β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ
π) |
19 | | fnpm 6655 |
. . . . 5
β’
βpm Fn (V Γ V) |
20 | | toponmax 13495 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π β π½) |
21 | 20 | elexd 2750 |
. . . . 5
β’ (π½ β (TopOnβπ) β π β V) |
22 | | cnex 7934 |
. . . . . 6
β’ β
β V |
23 | 22 | a1i 9 |
. . . . 5
β’ (π½ β (TopOnβπ) β β β
V) |
24 | | fnovex 5907 |
. . . . 5
β’ ((
βpm Fn (V Γ V) β§ π β V β§ β β V) β
(π
βpm β) β V) |
25 | 19, 21, 23, 24 | mp3an2i 1342 |
. . . 4
β’ (π½ β (TopOnβπ) β (π βpm β) β
V) |
26 | | xpexg 4740 |
. . . 4
β’ (((π βpm
β) β V β§ π
β π½) β ((π βpm
β) Γ π) β
V) |
27 | 25, 20, 26 | syl2anc 411 |
. . 3
β’ (π½ β (TopOnβπ) β ((π βpm β) Γ
π) β
V) |
28 | | ssexg 4142 |
. . 3
β’
(({β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ
π) β§ ((π βpm
β) Γ π) β
V) β {β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β V) |
29 | 18, 27, 28 | sylancr 414 |
. 2
β’ (π½ β (TopOnβπ) β {β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β V) |
30 | 2, 13, 14, 29 | fvmptd 5597 |
1
β’ (π½ β (TopOnβπ) β
(βπ‘βπ½) = {β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |