Step | Hyp | Ref
| Expression |
1 | | topontop 22414 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | | eqid 2732 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
3 | 2 | ist1 22824 |
. . . 4
β’ (π½ β Fre β (π½ β Top β§ βπ¦ β βͺ π½{π¦} β (Clsdβπ½))) |
4 | 3 | baib 536 |
. . 3
β’ (π½ β Top β (π½ β Fre β βπ¦ β βͺ π½{π¦} β (Clsdβπ½))) |
5 | 1, 4 | syl 17 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ¦ β βͺ π½{π¦} β (Clsdβπ½))) |
6 | | toponuni 22415 |
. . 3
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
7 | 6 | raleqdv 3325 |
. 2
β’ (π½ β (TopOnβπ) β (βπ¦ β π {π¦} β (Clsdβπ½) β βπ¦ β βͺ π½{π¦} β (Clsdβπ½))) |
8 | 1 | adantr 481 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β π½ β Top) |
9 | | eltop2 22477 |
. . . . . 6
β’ (π½ β Top β ((βͺ π½
β {π¦}) β π½ β βπ₯ β (βͺ π½
β {π¦})βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))) |
10 | 8, 9 | syl 17 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β ((βͺ
π½ β {π¦}) β π½ β βπ₯ β (βͺ π½ β {π¦})βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))) |
11 | 6 | eleq2d 2819 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β (π¦ β π β π¦ β βͺ π½)) |
12 | 11 | biimpa 477 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β π¦ β βͺ π½) |
13 | 12 | snssd 4812 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β {π¦} β βͺ π½) |
14 | 2 | iscld2 22531 |
. . . . . 6
β’ ((π½ β Top β§ {π¦} β βͺ π½)
β ({π¦} β
(Clsdβπ½) β
(βͺ π½ β {π¦}) β π½)) |
15 | 8, 13, 14 | syl2anc 584 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β ({π¦} β (Clsdβπ½) β (βͺ π½ β {π¦}) β π½)) |
16 | 6 | adantr 481 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β π = βͺ π½) |
17 | 16 | eleq2d 2819 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β (π₯ β π β π₯ β βͺ π½)) |
18 | 17 | imbi1d 341 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β ((π₯ β π β (π₯ β π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))) β (π₯ β βͺ π½ β (π₯ β π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))))) |
19 | | con1b 358 |
. . . . . . . . 9
β’ ((Β¬
π₯ = π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))) β (Β¬ βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})) β π₯ = π¦)) |
20 | | df-ne 2941 |
. . . . . . . . . 10
β’ (π₯ β π¦ β Β¬ π₯ = π¦) |
21 | 20 | imbi1i 349 |
. . . . . . . . 9
β’ ((π₯ β π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))) β (Β¬ π₯ = π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))) |
22 | | disjsn 4715 |
. . . . . . . . . . . . . . 15
β’ ((π β© {π¦}) = β
β Β¬ π¦ β π) |
23 | | elssuni 4941 |
. . . . . . . . . . . . . . . 16
β’ (π β π½ β π β βͺ π½) |
24 | | reldisj 4451 |
. . . . . . . . . . . . . . . 16
β’ (π β βͺ π½
β ((π β© {π¦}) = β
β π β (βͺ π½
β {π¦}))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π½ β ((π β© {π¦}) = β
β π β (βͺ π½ β {π¦}))) |
26 | 22, 25 | bitr3id 284 |
. . . . . . . . . . . . . 14
β’ (π β π½ β (Β¬ π¦ β π β π β (βͺ π½ β {π¦}))) |
27 | 26 | anbi2d 629 |
. . . . . . . . . . . . 13
β’ (π β π½ β ((π₯ β π β§ Β¬ π¦ β π) β (π₯ β π β§ π β (βͺ π½ β {π¦})))) |
28 | 27 | rexbiia 3092 |
. . . . . . . . . . . 12
β’
(βπ β
π½ (π₯ β π β§ Β¬ π¦ β π) β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))) |
29 | | rexanali 3102 |
. . . . . . . . . . . 12
β’
(βπ β
π½ (π₯ β π β§ Β¬ π¦ β π) β Β¬ βπ β π½ (π₯ β π β π¦ β π)) |
30 | 28, 29 | bitr3i 276 |
. . . . . . . . . . 11
β’
(βπ β
π½ (π₯ β π β§ π β (βͺ π½ β {π¦})) β Β¬ βπ β π½ (π₯ β π β π¦ β π)) |
31 | 30 | con2bii 357 |
. . . . . . . . . 10
β’
(βπ β
π½ (π₯ β π β π¦ β π) β Β¬ βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))) |
32 | 31 | imbi1i 349 |
. . . . . . . . 9
β’
((βπ β
π½ (π₯ β π β π¦ β π) β π₯ = π¦) β (Β¬ βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})) β π₯ = π¦)) |
33 | 19, 21, 32 | 3bitr4ri 303 |
. . . . . . . 8
β’
((βπ β
π½ (π₯ β π β π¦ β π) β π₯ = π¦) β (π₯ β π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))) |
34 | 33 | imbi2i 335 |
. . . . . . 7
β’ ((π₯ β π β (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) β (π₯ β π β (π₯ β π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))))) |
35 | | eldifsn 4790 |
. . . . . . . . 9
β’ (π₯ β (βͺ π½
β {π¦}) β (π₯ β βͺ π½
β§ π₯ β π¦)) |
36 | 35 | imbi1i 349 |
. . . . . . . 8
β’ ((π₯ β (βͺ π½
β {π¦}) β
βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))) β ((π₯ β βͺ π½ β§ π₯ β π¦) β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))) |
37 | | impexp 451 |
. . . . . . . 8
β’ (((π₯ β βͺ π½
β§ π₯ β π¦) β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))) β (π₯ β βͺ π½ β (π₯ β π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))))) |
38 | 36, 37 | bitri 274 |
. . . . . . 7
β’ ((π₯ β (βͺ π½
β {π¦}) β
βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))) β (π₯ β βͺ π½ β (π₯ β π¦ β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))))) |
39 | 18, 34, 38 | 3bitr4g 313 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β ((π₯ β π β (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) β (π₯ β (βͺ π½ β {π¦}) β βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦}))))) |
40 | 39 | ralbidv2 3173 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β (βπ₯ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β βπ₯ β (βͺ π½ β {π¦})βπ β π½ (π₯ β π β§ π β (βͺ π½ β {π¦})))) |
41 | 10, 15, 40 | 3bitr4d 310 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π¦ β π) β ({π¦} β (Clsdβπ½) β βπ₯ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
42 | 41 | ralbidva 3175 |
. . 3
β’ (π½ β (TopOnβπ) β (βπ¦ β π {π¦} β (Clsdβπ½) β βπ¦ β π βπ₯ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
43 | | ralcom 3286 |
. . 3
β’
(βπ¦ β
π βπ₯ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦) β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦)) |
44 | 42, 43 | bitrdi 286 |
. 2
β’ (π½ β (TopOnβπ) β (βπ¦ β π {π¦} β (Clsdβπ½) β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |
45 | 5, 7, 44 | 3bitr2d 306 |
1
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) |