| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2731 |
. . . 4
β’ (π β {π}) = (π β {π}) |
| 2 | | imaeq1 6055 |
. . . . 5
β’ (π£ = π β (π£ β {π}) = (π β {π})) |
| 3 | 2 | rspceeqv 3634 |
. . . 4
β’ ((π β π β§ (π β {π}) = (π β {π})) β βπ£ β π (π β {π}) = (π£ β {π})) |
| 4 | 1, 3 | mpan2 688 |
. . 3
β’ (π β π β βπ£ β π (π β {π}) = (π£ β {π})) |
| 5 | 4 | 3ad2ant2 1133 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β βπ£ β π (π β {π}) = (π£ β {π})) |
| 6 | | utoptop.1 |
. . . . . 6
β’ π½ = (unifTopβπ) |
| 7 | 6 | utopsnneip 23974 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβπ½)β{π}) = ran (π£ β π β¦ (π£ β {π}))) |
| 8 | 7 | 3adant2 1130 |
. . . 4
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β ((neiβπ½)β{π}) = ran (π£ β π β¦ (π£ β {π}))) |
| 9 | 8 | eleq2d 2818 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β ((π β {π}) β ((neiβπ½)β{π}) β (π β {π}) β ran (π£ β π β¦ (π£ β {π})))) |
| 10 | | imaexg 7909 |
. . . . 5
β’ (π β π β (π β {π}) β V) |
| 11 | | eqid 2731 |
. . . . . 6
β’ (π£ β π β¦ (π£ β {π})) = (π£ β π β¦ (π£ β {π})) |
| 12 | 11 | elrnmpt 5956 |
. . . . 5
β’ ((π β {π}) β V β ((π β {π}) β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π (π β {π}) = (π£ β {π}))) |
| 13 | 10, 12 | syl 17 |
. . . 4
β’ (π β π β ((π β {π}) β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π (π β {π}) = (π£ β {π}))) |
| 14 | 13 | 3ad2ant2 1133 |
. . 3
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β ((π β {π}) β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π (π β {π}) = (π£ β {π}))) |
| 15 | 9, 14 | bitrd 278 |
. 2
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β ((π β {π}) β ((neiβπ½)β{π}) β βπ£ β π (π β {π}) = (π£ β {π}))) |
| 16 | 5, 15 | mpbird 256 |
1
β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β {π}) β ((neiβπ½)β{π})) |
