Step | Hyp | Ref
| Expression |
1 | | connsuba 22923 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π) β ((π½ βΎt π) β Conn β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ ((π₯ β© π¦) β© π) = β
) β ((π₯ βͺ π¦) β© π) β π))) |
2 | | inss1 4228 |
. . . . . . 7
β’ (π₯ β© π¦) β π₯ |
3 | | toponss 22428 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π₯ β π½) β π₯ β π) |
4 | 3 | ad2ant2r 745 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β π₯ β π) |
5 | 2, 4 | sstrid 3993 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β (π₯ β© π¦) β π) |
6 | | reldisj 4451 |
. . . . . 6
β’ ((π₯ β© π¦) β π β (((π₯ β© π¦) β© π) = β
β (π₯ β© π¦) β (π β π))) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β (((π₯ β© π¦) β© π) = β
β (π₯ β© π¦) β (π β π))) |
8 | 7 | 3anbi3d 1442 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β (((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ ((π₯ β© π¦) β© π) = β
) β ((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ (π₯ β© π¦) β (π β π)))) |
9 | | sseqin2 4215 |
. . . . . . 7
β’ (π β (π₯ βͺ π¦) β ((π₯ βͺ π¦) β© π) = π) |
10 | 9 | a1i 11 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β (π β (π₯ βͺ π¦) β ((π₯ βͺ π¦) β© π) = π)) |
11 | 10 | bicomd 222 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β (((π₯ βͺ π¦) β© π) = π β π β (π₯ βͺ π¦))) |
12 | 11 | necon3abid 2977 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β (((π₯ βͺ π¦) β© π) β π β Β¬ π β (π₯ βͺ π¦))) |
13 | 8, 12 | imbi12d 344 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π β π) β§ (π₯ β π½ β§ π¦ β π½)) β ((((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ ((π₯ β© π¦) β© π) = β
) β ((π₯ βͺ π¦) β© π) β π) β (((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ (π₯ β© π¦) β (π β π)) β Β¬ π β (π₯ βͺ π¦)))) |
14 | 13 | 2ralbidva 3216 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π) β (βπ₯ β π½ βπ¦ β π½ (((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ ((π₯ β© π¦) β© π) = β
) β ((π₯ βͺ π¦) β© π) β π) β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ (π₯ β© π¦) β (π β π)) β Β¬ π β (π₯ βͺ π¦)))) |
15 | 1, 14 | bitrd 278 |
1
β’ ((π½ β (TopOnβπ) β§ π β π) β ((π½ βΎt π) β Conn β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π) β β
β§ (π¦ β© π) β β
β§ (π₯ β© π¦) β (π β π)) β Β¬ π β (π₯ βͺ π¦)))) |