Step | Hyp | Ref
| Expression |
1 | | fveq2 6897 |
. . . . . . 7
β’ (π = π½ β (neiβπ) = (neiβπ½)) |
2 | 1 | fveq1d 6899 |
. . . . . 6
β’ (π = π½ β ((neiβπ)β{π¦}) = ((neiβπ½)β{π¦})) |
3 | 2 | ineq1d 4211 |
. . . . 5
β’ (π = π½ β (((neiβπ)β{π¦}) β© π« π₯) = (((neiβπ½)β{π¦}) β© π« π₯)) |
4 | | oveq1 7427 |
. . . . . 6
β’ (π = π½ β (π βΎt π’) = (π½ βΎt π’)) |
5 | 4 | eleq1d 2814 |
. . . . 5
β’ (π = π½ β ((π βΎt π’) β π΄ β (π½ βΎt π’) β π΄)) |
6 | 3, 5 | rexeqbidv 3340 |
. . . 4
β’ (π = π½ β (βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
7 | 6 | ralbidv 3174 |
. . 3
β’ (π = π½ β (βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
8 | 7 | raleqbi1dv 3330 |
. 2
β’ (π = π½ β (βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
9 | | df-nlly 23384 |
. 2
β’
π-Locally π΄
= {π β Top β£
βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄} |
10 | 8, 9 | elrab2 3685 |
1
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |