Step | Hyp | Ref
| Expression |
1 | | lpfval.1 |
. . . . . . . . . . . . 13
β’ π = βͺ
π½ |
2 | 1 | neindisj 22620 |
. . . . . . . . . . . 12
β’ (((π½ β Top β§ π β π) β§ (π₯ β ((clsβπ½)βπ) β§ π β ((neiβπ½)β{π₯}))) β (π β© π) β β
) |
3 | 2 | expr 457 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (π β ((neiβπ½)β{π₯}) β (π β© π) β β
)) |
4 | 3 | adantr 481 |
. . . . . . . . . 10
β’ ((((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β§ Β¬ π₯ β π) β (π β ((neiβπ½)β{π₯}) β (π β© π) β β
)) |
5 | | difsn 4801 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π β (π β {π₯}) = π) |
6 | 5 | ineq2d 4212 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π β (π β© (π β {π₯})) = (π β© π)) |
7 | 6 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β π β ((π β© (π β {π₯})) β β
β (π β© π) β β
)) |
8 | 7 | adantl 482 |
. . . . . . . . . 10
β’ ((((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β§ Β¬ π₯ β π) β ((π β© (π β {π₯})) β β
β (π β© π) β β
)) |
9 | 4, 8 | sylibrd 258 |
. . . . . . . . 9
β’ ((((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β§ Β¬ π₯ β π) β (π β ((neiβπ½)β{π₯}) β (π β© (π β {π₯})) β β
)) |
10 | 9 | ex 413 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (Β¬ π₯ β π β (π β ((neiβπ½)β{π₯}) β (π β© (π β {π₯})) β β
))) |
11 | 10 | ralrimdv 3152 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (Β¬ π₯ β π β βπ β ((neiβπ½)β{π₯})(π β© (π β {π₯})) β β
)) |
12 | | simpll 765 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π½ β Top) |
13 | | simplr 767 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π β π) |
14 | 1 | clsss3 22562 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β π) |
15 | 14 | sselda 3982 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π₯ β π) |
16 | 1 | islp2 22648 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π β§ π₯ β π) β (π₯ β ((limPtβπ½)βπ) β βπ β ((neiβπ½)β{π₯})(π β© (π β {π₯})) β β
)) |
17 | 12, 13, 15, 16 | syl3anc 1371 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (π₯ β ((limPtβπ½)βπ) β βπ β ((neiβπ½)β{π₯})(π β© (π β {π₯})) β β
)) |
18 | 11, 17 | sylibrd 258 |
. . . . . 6
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (Β¬ π₯ β π β π₯ β ((limPtβπ½)βπ))) |
19 | 18 | orrd 861 |
. . . . 5
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (π₯ β π β¨ π₯ β ((limPtβπ½)βπ))) |
20 | | elun 4148 |
. . . . 5
β’ (π₯ β (π βͺ ((limPtβπ½)βπ)) β (π₯ β π β¨ π₯ β ((limPtβπ½)βπ))) |
21 | 19, 20 | sylibr 233 |
. . . 4
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π₯ β (π βͺ ((limPtβπ½)βπ))) |
22 | 21 | ex 413 |
. . 3
β’ ((π½ β Top β§ π β π) β (π₯ β ((clsβπ½)βπ) β π₯ β (π βͺ ((limPtβπ½)βπ)))) |
23 | 22 | ssrdv 3988 |
. 2
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β (π βͺ ((limPtβπ½)βπ))) |
24 | 1 | sscls 22559 |
. . 3
β’ ((π½ β Top β§ π β π) β π β ((clsβπ½)βπ)) |
25 | 1 | lpsscls 22644 |
. . 3
β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) β ((clsβπ½)βπ)) |
26 | 24, 25 | unssd 4186 |
. 2
β’ ((π½ β Top β§ π β π) β (π βͺ ((limPtβπ½)βπ)) β ((clsβπ½)βπ)) |
27 | 23, 26 | eqssd 3999 |
1
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) = (π βͺ ((limPtβπ½)βπ))) |