Step | Hyp | Ref
| Expression |
1 | | lpfval.1 |
. . . . . . . . . . . . 13
β’ π = βͺ
π½ |
2 | 1 | neindisj 22621 |
. . . . . . . . . . . 12
β’ (((π½ β Top β§ π β π) β§ (π₯ β ((clsβπ½)βπ) β§ π β ((neiβπ½)β{π₯}))) β (π β© π) β β
) |
3 | 2 | expr 458 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (π β ((neiβπ½)β{π₯}) β (π β© π) β β
)) |
4 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β§ Β¬ π₯ β π) β (π β ((neiβπ½)β{π₯}) β (π β© π) β β
)) |
5 | | difsn 4802 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β π β (π β {π₯}) = π) |
6 | 5 | ineq2d 4213 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π β (π β© (π β {π₯})) = (π β© π)) |
7 | 6 | neeq1d 3001 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β π β ((π β© (π β {π₯})) β β
β (π β© π) β β
)) |
8 | 7 | adantl 483 |
. . . . . . . . . 10
β’ ((((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β§ Β¬ π₯ β π) β ((π β© (π β {π₯})) β β
β (π β© π) β β
)) |
9 | 4, 8 | sylibrd 259 |
. . . . . . . . 9
β’ ((((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β§ Β¬ π₯ β π) β (π β ((neiβπ½)β{π₯}) β (π β© (π β {π₯})) β β
)) |
10 | 9 | ex 414 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (Β¬ π₯ β π β (π β ((neiβπ½)β{π₯}) β (π β© (π β {π₯})) β β
))) |
11 | 10 | ralrimdv 3153 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (Β¬ π₯ β π β βπ β ((neiβπ½)β{π₯})(π β© (π β {π₯})) β β
)) |
12 | | simpll 766 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π½ β Top) |
13 | | simplr 768 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π β π) |
14 | 1 | clsss3 22563 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β π) |
15 | 14 | sselda 3983 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π₯ β π) |
16 | 1 | islp2 22649 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π β§ π₯ β π) β (π₯ β ((limPtβπ½)βπ) β βπ β ((neiβπ½)β{π₯})(π β© (π β {π₯})) β β
)) |
17 | 12, 13, 15, 16 | syl3anc 1372 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (π₯ β ((limPtβπ½)βπ) β βπ β ((neiβπ½)β{π₯})(π β© (π β {π₯})) β β
)) |
18 | 11, 17 | sylibrd 259 |
. . . . . 6
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (Β¬ π₯ β π β π₯ β ((limPtβπ½)βπ))) |
19 | 18 | orrd 862 |
. . . . 5
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β (π₯ β π β¨ π₯ β ((limPtβπ½)βπ))) |
20 | | elun 4149 |
. . . . 5
β’ (π₯ β (π βͺ ((limPtβπ½)βπ)) β (π₯ β π β¨ π₯ β ((limPtβπ½)βπ))) |
21 | 19, 20 | sylibr 233 |
. . . 4
β’ (((π½ β Top β§ π β π) β§ π₯ β ((clsβπ½)βπ)) β π₯ β (π βͺ ((limPtβπ½)βπ))) |
22 | 21 | ex 414 |
. . 3
β’ ((π½ β Top β§ π β π) β (π₯ β ((clsβπ½)βπ) β π₯ β (π βͺ ((limPtβπ½)βπ)))) |
23 | 22 | ssrdv 3989 |
. 2
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β (π βͺ ((limPtβπ½)βπ))) |
24 | 1 | sscls 22560 |
. . 3
β’ ((π½ β Top β§ π β π) β π β ((clsβπ½)βπ)) |
25 | 1 | lpsscls 22645 |
. . 3
β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) β ((clsβπ½)βπ)) |
26 | 24, 25 | unssd 4187 |
. 2
β’ ((π½ β Top β§ π β π) β (π βͺ ((limPtβπ½)βπ)) β ((clsβπ½)βπ)) |
27 | 23, 26 | eqssd 4000 |
1
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) = (π βͺ ((limPtβπ½)βπ))) |