Step | Hyp | Ref
| Expression |
1 | | ist1-2 22682 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
2 | | toponmax 22259 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π β π½) |
3 | | eleq2 2826 |
. . . . . . . . 9
β’ (π = π β (π₯ β π β π₯ β π)) |
4 | 3 | intminss 4933 |
. . . . . . . 8
β’ ((π β π½ β§ π₯ β π) β β© {π β π½ β£ π₯ β π} β π) |
5 | 2, 4 | sylan 580 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π₯ β π) β β© {π β π½ β£ π₯ β π} β π) |
6 | 5 | sselda 3942 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π₯ β π) β§ π¦ β β© {π β π½ β£ π₯ β π}) β π¦ β π) |
7 | | biimt 360 |
. . . . . 6
β’ (π¦ β π β (π¦ β {π₯} β (π¦ β π β π¦ β {π₯}))) |
8 | 6, 7 | syl 17 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π₯ β π) β§ π¦ β β© {π β π½ β£ π₯ β π}) β (π¦ β {π₯} β (π¦ β π β π¦ β {π₯}))) |
9 | 8 | ralbidva 3170 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π₯ β π) β (βπ¦ β β© {π β π½ β£ π₯ β π}π¦ β {π₯} β βπ¦ β β© {π β π½ β£ π₯ β π} (π¦ β π β π¦ β {π₯}))) |
10 | | id 22 |
. . . . . . . . 9
β’ (π₯ β π β π₯ β π) |
11 | 10 | rgenw 3066 |
. . . . . . . 8
β’
βπ β
π½ (π₯ β π β π₯ β π) |
12 | | vex 3447 |
. . . . . . . . 9
β’ π₯ β V |
13 | 12 | elintrab 4919 |
. . . . . . . 8
β’ (π₯ β β© {π
β π½ β£ π₯ β π} β βπ β π½ (π₯ β π β π₯ β π)) |
14 | 11, 13 | mpbir 230 |
. . . . . . 7
β’ π₯ β β© {π
β π½ β£ π₯ β π} |
15 | | snssi 4766 |
. . . . . . 7
β’ (π₯ β β© {π
β π½ β£ π₯ β π} β {π₯} β β© {π β π½ β£ π₯ β π}) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
β’ {π₯} β β© {π
β π½ β£ π₯ β π} |
17 | | eqss 3957 |
. . . . . 6
β’ (β© {π
β π½ β£ π₯ β π} = {π₯} β (β© {π β π½ β£ π₯ β π} β {π₯} β§ {π₯} β β© {π β π½ β£ π₯ β π})) |
18 | 16, 17 | mpbiran2 708 |
. . . . 5
β’ (β© {π
β π½ β£ π₯ β π} = {π₯} β β© {π β π½ β£ π₯ β π} β {π₯}) |
19 | | dfss3 3930 |
. . . . 5
β’ (β© {π
β π½ β£ π₯ β π} β {π₯} β βπ¦ β β© {π β π½ β£ π₯ β π}π¦ β {π₯}) |
20 | 18, 19 | bitri 274 |
. . . 4
β’ (β© {π
β π½ β£ π₯ β π} = {π₯} β βπ¦ β β© {π β π½ β£ π₯ β π}π¦ β {π₯}) |
21 | | vex 3447 |
. . . . . . . 8
β’ π¦ β V |
22 | 21 | elintrab 4919 |
. . . . . . 7
β’ (π¦ β β© {π
β π½ β£ π₯ β π} β βπ β π½ (π₯ β π β π¦ β π)) |
23 | | velsn 4600 |
. . . . . . . 8
β’ (π¦ β {π₯} β π¦ = π₯) |
24 | | equcom 2021 |
. . . . . . . 8
β’ (π¦ = π₯ β π₯ = π¦) |
25 | 23, 24 | bitri 274 |
. . . . . . 7
β’ (π¦ β {π₯} β π₯ = π¦) |
26 | 22, 25 | imbi12i 350 |
. . . . . 6
β’ ((π¦ β β© {π
β π½ β£ π₯ β π} β π¦ β {π₯}) β (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) |
27 | 26 | ralbii 3094 |
. . . . 5
β’
(βπ¦ β
π (π¦ β β© {π β π½ β£ π₯ β π} β π¦ β {π₯}) β βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) |
28 | | ralcom3 3098 |
. . . . 5
β’
(βπ¦ β
π (π¦ β β© {π β π½ β£ π₯ β π} β π¦ β {π₯}) β βπ¦ β β© {π β π½ β£ π₯ β π} (π¦ β π β π¦ β {π₯})) |
29 | 27, 28 | bitr3i 276 |
. . . 4
β’
(βπ¦ β
π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β βπ¦ β β© {π β π½ β£ π₯ β π} (π¦ β π β π¦ β {π₯})) |
30 | 9, 20, 29 | 3bitr4g 313 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π₯ β π) β (β©
{π β π½ β£ π₯ β π} = {π₯} β βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
31 | 30 | ralbidva 3170 |
. 2
β’ (π½ β (TopOnβπ) β (βπ₯ β π β© {π β π½ β£ π₯ β π} = {π₯} β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
32 | 1, 31 | bitr4d 281 |
1
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π β© {π β π½ β£ π₯ β π} = {π₯})) |