Step | Hyp | Ref
| Expression |
1 | | df-lm 13693 |
. . 3
β’
βπ‘ = (π β Top β¦ {β¨π, π₯β© β£ (π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |
2 | 1 | a1i 9 |
. 2
β’ (π½ β (TopOnβπ) β
βπ‘ = (π β Top β¦ {β¨π, π₯β© β£ (π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))})) |
3 | | simpr 110 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π = π½) β π = π½) |
4 | 3 | unieqd 3821 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π = π½) β βͺ π = βͺ
π½) |
5 | | toponuni 13518 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
6 | 5 | adantr 276 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π = π½) β π = βͺ π½) |
7 | 4, 6 | eqtr4d 2213 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π = π½) β βͺ π = π) |
8 | 7 | oveq1d 5890 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π = π½) β (βͺ π βpm
β) = (π
βpm β)) |
9 | 8 | eleq2d 2247 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (π β (βͺ π βpm
β) β π β
(π
βpm β))) |
10 | 7 | eleq2d 2247 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (π₯ β βͺ π β π₯ β π)) |
11 | 3 | raleqdv 2679 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π = π½) β (βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’) β βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))) |
12 | 9, 10, 11 | 3anbi123d 1312 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π = π½) β ((π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)) β (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)))) |
13 | 12 | opabbidv 4070 |
. 2
β’ ((π½ β (TopOnβπ) β§ π = π½) β {β¨π, π₯β© β£ (π β (βͺ π βpm
β) β§ π₯ β
βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} = {β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |
14 | | topontop 13517 |
. 2
β’ (π½ β (TopOnβπ) β π½ β Top) |
15 | | df-3an 980 |
. . . . 5
β’ ((π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’)) β ((π β (π βpm β) β§
π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))) |
16 | 15 | opabbii 4071 |
. . . 4
β’
{β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} = {β¨π, π₯β© β£ ((π β (π βpm β) β§
π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} |
17 | | opabssxp 4701 |
. . . 4
β’
{β¨π, π₯β© β£ ((π β (π βpm β) β§
π₯ β π) β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ
π) |
18 | 16, 17 | eqsstri 3188 |
. . 3
β’
{β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))} β ((π βpm β) Γ
π) |
19 | | fnpm 6656 |
. . . . 5
β’
βpm Fn (V Γ V) |
20 | | toponmax 13528 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π β π½) |
21 | 20 | elexd 2751 |
. . . . 5
β’ (π½ β (TopOnβπ) β π β V) |
22 | | cnex 7935 |
. . . . . 6
β’ β
β V |
23 | 22 | a1i 9 |
. . . . 5
β’ (π½ β (TopOnβπ) β β β
V) |
24 | | fnovex 5908 |
. . . . 5
β’ ((
βpm Fn (V Γ V) β§ π β V β§ β β V) β
(π
βpm β) β V) |
25 | 19, 21, 23, 24 | mp3an2i 1342 |
. . . 4
β’ (π½ β (TopOnβπ) β (π βpm β) β
V) |
26 | | xpexg 4741 |
. . . 4
β’ (((π βpm
β) β V β§ π
β π½) β ((π βpm
β) Γ π) β
V) |
27 | 25, 20, 26 | syl2anc 411 |
. . 3
β’ (π½ β (TopOnβπ) β ((π βpm β) Γ
π) β
V) |
28 | | ssexg 4143 |
. . 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 5598 |
1
β’ (π½ β (TopOnβπ) β
(βπ‘βπ½) = {β¨π, π₯β© β£ (π β (π βpm β) β§
π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) |