Step | Hyp | Ref
| Expression |
1 | | simp3 1139 |
. . . . . . 7
β’ ((π½ β Top β§ π β π β§ π β π) β π β π) |
2 | 1 | ssdifssd 4143 |
. . . . . 6
β’ ((π½ β Top β§ π β π β§ π β π) β (π β {π₯}) β π) |
3 | | restcls.1 |
. . . . . . 7
β’ π = βͺ
π½ |
4 | | restcls.2 |
. . . . . . 7
β’ πΎ = (π½ βΎt π) |
5 | 3, 4 | restcls 22685 |
. . . . . 6
β’ ((π½ β Top β§ π β π β§ (π β {π₯}) β π) β ((clsβπΎ)β(π β {π₯})) = (((clsβπ½)β(π β {π₯})) β© π)) |
6 | 2, 5 | syld3an3 1410 |
. . . . 5
β’ ((π½ β Top β§ π β π β§ π β π) β ((clsβπΎ)β(π β {π₯})) = (((clsβπ½)β(π β {π₯})) β© π)) |
7 | 6 | eleq2d 2820 |
. . . 4
β’ ((π½ β Top β§ π β π β§ π β π) β (π₯ β ((clsβπΎ)β(π β {π₯})) β π₯ β (((clsβπ½)β(π β {π₯})) β© π))) |
8 | | elin 3965 |
. . . 4
β’ (π₯ β (((clsβπ½)β(π β {π₯})) β© π) β (π₯ β ((clsβπ½)β(π β {π₯})) β§ π₯ β π)) |
9 | 7, 8 | bitrdi 287 |
. . 3
β’ ((π½ β Top β§ π β π β§ π β π) β (π₯ β ((clsβπΎ)β(π β {π₯})) β (π₯ β ((clsβπ½)β(π β {π₯})) β§ π₯ β π))) |
10 | | simp1 1137 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π β§ π β π) β π½ β Top) |
11 | 3 | toptopon 22419 |
. . . . . . . 8
β’ (π½ β Top β π½ β (TopOnβπ)) |
12 | 10, 11 | sylib 217 |
. . . . . . 7
β’ ((π½ β Top β§ π β π β§ π β π) β π½ β (TopOnβπ)) |
13 | | simp2 1138 |
. . . . . . 7
β’ ((π½ β Top β§ π β π β§ π β π) β π β π) |
14 | | resttopon 22665 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π) β (π½ βΎt π) β (TopOnβπ)) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . . 6
β’ ((π½ β Top β§ π β π β§ π β π) β (π½ βΎt π) β (TopOnβπ)) |
16 | 4, 15 | eqeltrid 2838 |
. . . . 5
β’ ((π½ β Top β§ π β π β§ π β π) β πΎ β (TopOnβπ)) |
17 | | topontop 22415 |
. . . . 5
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
18 | 16, 17 | syl 17 |
. . . 4
β’ ((π½ β Top β§ π β π β§ π β π) β πΎ β Top) |
19 | | toponuni 22416 |
. . . . . 6
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
20 | 16, 19 | syl 17 |
. . . . 5
β’ ((π½ β Top β§ π β π β§ π β π) β π = βͺ πΎ) |
21 | 1, 20 | sseqtrd 4023 |
. . . 4
β’ ((π½ β Top β§ π β π β§ π β π) β π β βͺ πΎ) |
22 | | eqid 2733 |
. . . . 5
β’ βͺ πΎ =
βͺ πΎ |
23 | 22 | islp 22644 |
. . . 4
β’ ((πΎ β Top β§ π β βͺ πΎ)
β (π₯ β
((limPtβπΎ)βπ) β π₯ β ((clsβπΎ)β(π β {π₯})))) |
24 | 18, 21, 23 | syl2anc 585 |
. . 3
β’ ((π½ β Top β§ π β π β§ π β π) β (π₯ β ((limPtβπΎ)βπ) β π₯ β ((clsβπΎ)β(π β {π₯})))) |
25 | | elin 3965 |
. . . 4
β’ (π₯ β (((limPtβπ½)βπ) β© π) β (π₯ β ((limPtβπ½)βπ) β§ π₯ β π)) |
26 | 1, 13 | sstrd 3993 |
. . . . . 6
β’ ((π½ β Top β§ π β π β§ π β π) β π β π) |
27 | 3 | islp 22644 |
. . . . . 6
β’ ((π½ β Top β§ π β π) β (π₯ β ((limPtβπ½)βπ) β π₯ β ((clsβπ½)β(π β {π₯})))) |
28 | 10, 26, 27 | syl2anc 585 |
. . . . 5
β’ ((π½ β Top β§ π β π β§ π β π) β (π₯ β ((limPtβπ½)βπ) β π₯ β ((clsβπ½)β(π β {π₯})))) |
29 | 28 | anbi1d 631 |
. . . 4
β’ ((π½ β Top β§ π β π β§ π β π) β ((π₯ β ((limPtβπ½)βπ) β§ π₯ β π) β (π₯ β ((clsβπ½)β(π β {π₯})) β§ π₯ β π))) |
30 | 25, 29 | bitrid 283 |
. . 3
β’ ((π½ β Top β§ π β π β§ π β π) β (π₯ β (((limPtβπ½)βπ) β© π) β (π₯ β ((clsβπ½)β(π β {π₯})) β§ π₯ β π))) |
31 | 9, 24, 30 | 3bitr4d 311 |
. 2
β’ ((π½ β Top β§ π β π β§ π β π) β (π₯ β ((limPtβπΎ)βπ) β π₯ β (((limPtβπ½)βπ) β© π))) |
32 | 31 | eqrdv 2731 |
1
β’ ((π½ β Top β§ π β π β§ π β π) β ((limPtβπΎ)βπ) = (((limPtβπ½)βπ) β© π)) |