Step | Hyp | Ref
| Expression |
1 | | ssel 3941 |
. . . . . . 7
β’ (π΄ β π΅ β ((π βΎt π’) β π΄ β (π βΎt π’) β π΅)) |
2 | 1 | reximdv 3164 |
. . . . . 6
β’ (π΄ β π΅ β (βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅)) |
3 | 2 | ralimdv 3163 |
. . . . 5
β’ (π΄ β π΅ β (βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅)) |
4 | 3 | ralimdv 3163 |
. . . 4
β’ (π΄ β π΅ β (βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅)) |
5 | 4 | anim2d 613 |
. . 3
β’ (π΄ β π΅ β ((π β Top β§ βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄) β (π β Top β§ βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅))) |
6 | | isnlly 22843 |
. . 3
β’ (π β π-Locally π΄ β (π β Top β§ βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄)) |
7 | | isnlly 22843 |
. . 3
β’ (π β π-Locally π΅ β (π β Top β§ βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅)) |
8 | 5, 6, 7 | 3imtr4g 296 |
. 2
β’ (π΄ β π΅ β (π β π-Locally π΄ β π β π-Locally π΅)) |
9 | 8 | ssrdv 3954 |
1
β’ (π΄ β π΅ β π-Locally π΄ β π-Locally π΅) |