Step | Hyp | Ref
| Expression |
1 | | utopval 23607 |
. . . 4
β’ (π β (UnifOnβπ) β (unifTopβπ) = {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π}) |
2 | | ssrab2 4041 |
. . . 4
β’ {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π} β π« π |
3 | 1, 2 | eqsstrdi 4002 |
. . 3
β’ (π β (UnifOnβπ) β (unifTopβπ) β π« π) |
4 | | ssidd 3971 |
. . . . 5
β’ (π β (UnifOnβπ) β π β π) |
5 | | ustssxp 23579 |
. . . . . . . . 9
β’ ((π β (UnifOnβπ) β§ π£ β π) β π£ β (π Γ π)) |
6 | | imassrn 6028 |
. . . . . . . . . 10
β’ (π£ β {π₯}) β ran π£ |
7 | | rnss 5898 |
. . . . . . . . . . 11
β’ (π£ β (π Γ π) β ran π£ β ran (π Γ π)) |
8 | | rnxpid 6129 |
. . . . . . . . . . 11
β’ ran
(π Γ π) = π |
9 | 7, 8 | sseqtrdi 3998 |
. . . . . . . . . 10
β’ (π£ β (π Γ π) β ran π£ β π) |
10 | 6, 9 | sstrid 3959 |
. . . . . . . . 9
β’ (π£ β (π Γ π) β (π£ β {π₯}) β π) |
11 | 5, 10 | syl 17 |
. . . . . . . 8
β’ ((π β (UnifOnβπ) β§ π£ β π) β (π£ β {π₯}) β π) |
12 | 11 | ralrimiva 3140 |
. . . . . . 7
β’ (π β (UnifOnβπ) β βπ£ β π (π£ β {π₯}) β π) |
13 | | ustne0 23588 |
. . . . . . . 8
β’ (π β (UnifOnβπ) β π β β
) |
14 | | r19.2zb 4457 |
. . . . . . . 8
β’ (π β β
β
(βπ£ β π (π£ β {π₯}) β π β βπ£ β π (π£ β {π₯}) β π)) |
15 | 13, 14 | sylib 217 |
. . . . . . 7
β’ (π β (UnifOnβπ) β (βπ£ β π (π£ β {π₯}) β π β βπ£ β π (π£ β {π₯}) β π)) |
16 | 12, 15 | mpd 15 |
. . . . . 6
β’ (π β (UnifOnβπ) β βπ£ β π (π£ β {π₯}) β π) |
17 | 16 | ralrimivw 3144 |
. . . . 5
β’ (π β (UnifOnβπ) β βπ₯ β π βπ£ β π (π£ β {π₯}) β π) |
18 | | elutop 23608 |
. . . . 5
β’ (π β (UnifOnβπ) β (π β (unifTopβπ) β (π β π β§ βπ₯ β π βπ£ β π (π£ β {π₯}) β π))) |
19 | 4, 17, 18 | mpbir2and 712 |
. . . 4
β’ (π β (UnifOnβπ) β π β (unifTopβπ)) |
20 | | elpwuni 5069 |
. . . 4
β’ (π β (unifTopβπ) β ((unifTopβπ) β π« π β βͺ (unifTopβπ) = π)) |
21 | 19, 20 | syl 17 |
. . 3
β’ (π β (UnifOnβπ) β ((unifTopβπ) β π« π β βͺ (unifTopβπ) = π)) |
22 | 3, 21 | mpbid 231 |
. 2
β’ (π β (UnifOnβπ) β βͺ (unifTopβπ) = π) |
23 | 22 | eqcomd 2739 |
1
β’ (π β (UnifOnβπ) β π = βͺ
(unifTopβπ)) |