Step | Hyp | Ref
| Expression |
1 | | isnlly 22843 |
. . . 4
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) |
2 | 1 | simprbi 498 |
. . 3
β’ (π½ β π-Locally π΄ β βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄) |
3 | | pweq 4578 |
. . . . . . 7
β’ (π₯ = π β π« π₯ = π« π) |
4 | 3 | ineq2d 4176 |
. . . . . 6
β’ (π₯ = π β (((neiβπ½)β{π¦}) β© π« π₯) = (((neiβπ½)β{π¦}) β© π« π)) |
5 | 4 | rexeqdv 3313 |
. . . . 5
β’ (π₯ = π β (βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄ β βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄)) |
6 | 5 | raleqbi1dv 3306 |
. . . 4
β’ (π₯ = π β (βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄ β βπ¦ β π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄)) |
7 | 6 | rspccva 3582 |
. . 3
β’
((βπ₯ β
π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄ β§ π β π½) β βπ¦ β π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄) |
8 | 2, 7 | sylan 581 |
. 2
β’ ((π½ β π-Locally π΄ β§ π β π½) β βπ¦ β π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄) |
9 | | elin 3930 |
. . . . . . 7
β’ (π’ β (((neiβπ½)β{π¦}) β© π« π) β (π’ β ((neiβπ½)β{π¦}) β§ π’ β π« π)) |
10 | | sneq 4600 |
. . . . . . . . . 10
β’ (π¦ = π β {π¦} = {π}) |
11 | 10 | fveq2d 6850 |
. . . . . . . . 9
β’ (π¦ = π β ((neiβπ½)β{π¦}) = ((neiβπ½)β{π})) |
12 | 11 | eleq2d 2820 |
. . . . . . . 8
β’ (π¦ = π β (π’ β ((neiβπ½)β{π¦}) β π’ β ((neiβπ½)β{π}))) |
13 | | velpw 4569 |
. . . . . . . . 9
β’ (π’ β π« π β π’ β π) |
14 | 13 | a1i 11 |
. . . . . . . 8
β’ (π¦ = π β (π’ β π« π β π’ β π)) |
15 | 12, 14 | anbi12d 632 |
. . . . . . 7
β’ (π¦ = π β ((π’ β ((neiβπ½)β{π¦}) β§ π’ β π« π) β (π’ β ((neiβπ½)β{π}) β§ π’ β π))) |
16 | 9, 15 | bitrid 283 |
. . . . . 6
β’ (π¦ = π β (π’ β (((neiβπ½)β{π¦}) β© π« π) β (π’ β ((neiβπ½)β{π}) β§ π’ β π))) |
17 | 16 | anbi1d 631 |
. . . . 5
β’ (π¦ = π β ((π’ β (((neiβπ½)β{π¦}) β© π« π) β§ (π½ βΎt π’) β π΄) β ((π’ β ((neiβπ½)β{π}) β§ π’ β π) β§ (π½ βΎt π’) β π΄))) |
18 | | anass 470 |
. . . . 5
β’ (((π’ β ((neiβπ½)β{π}) β§ π’ β π) β§ (π½ βΎt π’) β π΄) β (π’ β ((neiβπ½)β{π}) β§ (π’ β π β§ (π½ βΎt π’) β π΄))) |
19 | 17, 18 | bitrdi 287 |
. . . 4
β’ (π¦ = π β ((π’ β (((neiβπ½)β{π¦}) β© π« π) β§ (π½ βΎt π’) β π΄) β (π’ β ((neiβπ½)β{π}) β§ (π’ β π β§ (π½ βΎt π’) β π΄)))) |
20 | 19 | rexbidv2 3168 |
. . 3
β’ (π¦ = π β (βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄ β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄))) |
21 | 20 | rspccva 3582 |
. 2
β’
((βπ¦ β
π βπ’ β (((neiβπ½)β{π¦}) β© π« π)(π½ βΎt π’) β π΄ β§ π β π) β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄)) |
22 | 8, 21 | stoic3 1779 |
1
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄)) |