Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
2 | 1 | eleq2d 2818 |
. . . . . 6
β’ (π = π β (π β (πβπ) β π β (πβπ))) |
3 | 2 | cbvralvw 3233 |
. . . . 5
β’
(βπ β
π π β (πβπ) β βπ β π π β (πβπ)) |
4 | | eleq1w 2815 |
. . . . . 6
β’ (π = π β (π β (πβπ) β π β (πβπ))) |
5 | 4 | raleqbi1dv 3332 |
. . . . 5
β’ (π = π β (βπ β π π β (πβπ) β βπ β π π β (πβπ))) |
6 | 3, 5 | bitr3id 285 |
. . . 4
β’ (π = π β (βπ β π π β (πβπ) β βπ β π π β (πβπ))) |
7 | 6 | cbvrabv 3441 |
. . 3
β’ {π β π« π β£ βπ β π π β (πβπ)} = {π β π« π β£ βπ β π π β (πβπ)} |
8 | | utopustuq.1 |
. . . 4
β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) |
9 | 8 | ustuqtop0 23966 |
. . 3
β’ (π β (UnifOnβπ) β π:πβΆπ« π« π) |
10 | 8 | ustuqtop1 23967 |
. . 3
β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) |
11 | 8 | ustuqtop2 23968 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β (fiβ(πβπ)) β (πβπ)) |
12 | 8 | ustuqtop3 23969 |
. . 3
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β π β π) |
13 | 8 | ustuqtop4 23970 |
. . 3
β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ₯ β π π β (πβπ₯)) |
14 | 8 | ustuqtop5 23971 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π) β π β (πβπ)) |
15 | 7, 9, 10, 11, 12, 13, 14 | neiptopreu 22858 |
. 2
β’ (π β (UnifOnβπ) β β!π β (TopOnβπ)π = (π β π β¦ ((neiβπ)β{π}))) |
16 | 9 | feqmptd 6960 |
. . . . 5
β’ (π β (UnifOnβπ) β π = (π β π β¦ (πβπ))) |
17 | 16 | eqeq1d 2733 |
. . . 4
β’ (π β (UnifOnβπ) β (π = (π β π β¦ ((neiβπ)β{π})) β (π β π β¦ (πβπ)) = (π β π β¦ ((neiβπ)β{π})))) |
18 | | fvex 6904 |
. . . . . 6
β’ (πβπ) β V |
19 | 18 | rgenw 3064 |
. . . . 5
β’
βπ β
π (πβπ) β V |
20 | | mpteqb 7017 |
. . . . 5
β’
(βπ β
π (πβπ) β V β ((π β π β¦ (πβπ)) = (π β π β¦ ((neiβπ)β{π})) β βπ β π (πβπ) = ((neiβπ)β{π}))) |
21 | 19, 20 | ax-mp 5 |
. . . 4
β’ ((π β π β¦ (πβπ)) = (π β π β¦ ((neiβπ)β{π})) β βπ β π (πβπ) = ((neiβπ)β{π})) |
22 | 17, 21 | bitrdi 287 |
. . 3
β’ (π β (UnifOnβπ) β (π = (π β π β¦ ((neiβπ)β{π})) β βπ β π (πβπ) = ((neiβπ)β{π}))) |
23 | 22 | reubidv 3393 |
. 2
β’ (π β (UnifOnβπ) β (β!π β (TopOnβπ)π = (π β π β¦ ((neiβπ)β{π})) β β!π β (TopOnβπ)βπ β π (πβπ) = ((neiβπ)β{π}))) |
24 | 15, 23 | mpbid 231 |
1
β’ (π β (UnifOnβπ) β β!π β (TopOnβπ)βπ β π (πβπ) = ((neiβπ)β{π})) |