| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-utop 24056 |
. 2
β’ unifTop =
(π’ β βͺ ran UnifOn β¦ {π β π« dom βͺ π’
β£ βπ₯ β
π βπ£ β π’ (π£ β {π₯}) β π}) |
| 2 | | simpr 484 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π’ = π) β π’ = π) |
| 3 | 2 | unieqd 4922 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π’ = π) β βͺ π’ = βͺ
π) |
| 4 | 3 | dmeqd 5905 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π’ = π) β dom βͺ
π’ = dom βͺ π) |
| 5 | | ustbas2 24050 |
. . . . . 6
β’ (π β (UnifOnβπ) β π = dom βͺ π) |
| 6 | 5 | adantr 480 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π’ = π) β π = dom βͺ π) |
| 7 | 4, 6 | eqtr4d 2774 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π’ = π) β dom βͺ
π’ = π) |
| 8 | 7 | pweqd 4619 |
. . 3
β’ ((π β (UnifOnβπ) β§ π’ = π) β π« dom βͺ π’ =
π« π) |
| 9 | 2 | rexeqdv 3325 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π’ = π) β (βπ£ β π’ (π£ β {π₯}) β π β βπ£ β π (π£ β {π₯}) β π)) |
| 10 | 9 | ralbidv 3176 |
. . 3
β’ ((π β (UnifOnβπ) β§ π’ = π) β (βπ₯ β π βπ£ β π’ (π£ β {π₯}) β π β βπ₯ β π βπ£ β π (π£ β {π₯}) β π)) |
| 11 | 8, 10 | rabeqbidv 3448 |
. 2
β’ ((π β (UnifOnβπ) β§ π’ = π) β {π β π« dom βͺ π’
β£ βπ₯ β
π βπ£ β π’ (π£ β {π₯}) β π} = {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π}) |
| 12 | | elfvunirn 6923 |
. 2
β’ (π β (UnifOnβπ) β π β βͺ ran
UnifOn) |
| 13 | | elfvex 6929 |
. . 3
β’ (π β (UnifOnβπ) β π β V) |
| 14 | | pwexg 5376 |
. . 3
β’ (π β V β π« π β V) |
| 15 | | rabexg 5331 |
. . 3
β’
(π« π β
V β {π β
π« π β£
βπ₯ β π βπ£ β π (π£ β {π₯}) β π} β V) |
| 16 | 13, 14, 15 | 3syl 18 |
. 2
β’ (π β (UnifOnβπ) β {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π} β V) |
| 17 | 1, 11, 12, 16 | fvmptd2 7006 |
1
β’ (π β (UnifOnβπ) β (unifTopβπ) = {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π}) |
