Step | Hyp | Ref
| Expression |
1 | | isnlly 22972 |
. . . 4
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
2 | 1 | simprbi 497 |
. . 3
β’ (π½ β π-Locally π΄ β βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄) |
3 | | pweq 4616 |
. . . . . . 7
β’ (π₯ = π β π« π₯ = π« π) |
4 | 3 | ineq2d 4212 |
. . . . . 6
β’ (π₯ = π β (((neiβπ½)β{π¦}) β© π« π₯) = (((neiβπ½)β{π¦}) β© π« π)) |
5 | 4 | rexeqdv 3326 |
. . . . 5
β’ (π₯ = π β (βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄ β βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄)) |
6 | 5 | raleqbi1dv 3333 |
. . . 4
β’ (π₯ = π β (βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄ β βπ¦ β π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄)) |
7 | 6 | rspccva 3611 |
. . 3
β’
((βπ₯ β
π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄ β§ π β π½) β βπ¦ β π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄) |
8 | 2, 7 | sylan 580 |
. 2
β’ ((π½ β π-Locally π΄ β§ π β π½) β βπ¦ β π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄) |
9 | | elin 3964 |
. . . . . . 7
β’ (π’ β (((neiβπ½)β{π¦}) β© π« π) β (π’ β ((neiβπ½)β{π¦}) β§ π’ β π« π)) |
10 | | sneq 4638 |
. . . . . . . . . 10
β’ (π¦ = π β {π¦} = {π}) |
11 | 10 | fveq2d 6895 |
. . . . . . . . 9
β’ (π¦ = π β ((neiβπ½)β{π¦}) = ((neiβπ½)β{π})) |
12 | 11 | eleq2d 2819 |
. . . . . . . 8
β’ (π¦ = π β (π’ β ((neiβπ½)β{π¦}) β π’ β ((neiβπ½)β{π}))) |
13 | | velpw 4607 |
. . . . . . . . 9
β’ (π’ β π« π β π’ β π) |
14 | 13 | a1i 11 |
. . . . . . . 8
β’ (π¦ = π β (π’ β π« π β π’ β π)) |
15 | 12, 14 | anbi12d 631 |
. . . . . . 7
β’ (π¦ = π β ((π’ β ((neiβπ½)β{π¦}) β§ π’ β π« π) β (π’ β ((neiβπ½)β{π}) β§ π’ β π))) |
16 | 9, 15 | bitrid 282 |
. . . . . 6
β’ (π¦ = π β (π’ β (((neiβπ½)β{π¦}) β© π« π) β (π’ β ((neiβπ½)β{π}) β§ π’ β π))) |
17 | 16 | anbi1d 630 |
. . . . 5
β’ (π¦ = π β ((π’ β (((neiβπ½)β{π¦}) β© π« π) β§ (π½ βΎt π’) β π΄) β ((π’ β ((neiβπ½)β{π}) β§ π’ β π) β§ (π½ βΎt π’) β π΄))) |
18 | | anass 469 |
. . . . 5
β’ (((π’ β ((neiβπ½)β{π}) β§ π’ β π) β§ (π½ βΎt π’) β π΄) β (π’ β ((neiβπ½)β{π}) β§ (π’ β π β§ (π½ βΎt π’) β π΄))) |
19 | 17, 18 | bitrdi 286 |
. . . 4
β’ (π¦ = π β ((π’ β (((neiβπ½)β{π¦}) β© π« π) β§ (π½ βΎt π’) β π΄) β (π’ β ((neiβπ½)β{π}) β§ (π’ β π β§ (π½ βΎt π’) β π΄)))) |
20 | 19 | rexbidv2 3174 |
. . 3
β’ (π¦ = π β (βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄ β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄))) |
21 | 20 | rspccva 3611 |
. 2
β’
((βπ¦ β
π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄ β§ π β π) β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄)) |
22 | 8, 21 | stoic3 1778 |
1
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄)) |