Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . 7
β’ (π = π½ β (neiβπ) = (neiβπ½)) |
2 | 1 | fveq1d 6845 |
. . . . . 6
β’ (π = π½ β ((neiβπ)β{π¦}) = ((neiβπ½)β{π¦})) |
3 | 2 | ineq1d 4172 |
. . . . 5
β’ (π = π½ β (((neiβπ)β{π¦}) β© π« π₯) = (((neiβπ½)β{π¦}) β© π« π₯)) |
4 | | oveq1 7365 |
. . . . . 6
β’ (π = π½ β (π βΎt π’) = (π½ βΎt π’)) |
5 | 4 | eleq1d 2819 |
. . . . 5
β’ (π = π½ β ((π βΎt π’) β π΄ β (π½ βΎt π’) β π΄)) |
6 | 3, 5 | rexeqbidv 3319 |
. . . 4
β’ (π = π½ β (βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
7 | 6 | ralbidv 3171 |
. . 3
β’ (π = π½ β (βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
8 | 7 | raleqbi1dv 3306 |
. 2
β’ (π = π½ β (βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
9 | | df-nlly 22834 |
. 2
β’
π-Locally π΄
= {π β Top β£
βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄} |
10 | 8, 9 | elrab2 3649 |
1
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |