Step | Hyp | Ref
| Expression |
1 | | nconnsubb.9 |
. 2
β’ (π β π΄ β (π βͺ π)) |
2 | | nconnsubb.2 |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
3 | | nconnsubb.3 |
. . . 4
β’ (π β π΄ β π) |
4 | | connsuba 22787 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((π½ βΎt π΄) β Conn β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄))) |
5 | 2, 3, 4 | syl2anc 585 |
. . 3
β’ (π β ((π½ βΎt π΄) β Conn β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄))) |
6 | | nconnsubb.6 |
. . . . 5
β’ (π β (π β© π΄) β β
) |
7 | | nconnsubb.7 |
. . . . 5
β’ (π β (π β© π΄) β β
) |
8 | | nconnsubb.8 |
. . . . 5
β’ (π β ((π β© π) β© π΄) = β
) |
9 | 6, 7, 8 | 3jca 1129 |
. . . 4
β’ (π β ((π β© π΄) β β
β§ (π β© π΄) β β
β§ ((π β© π) β© π΄) = β
)) |
10 | | nconnsubb.4 |
. . . . 5
β’ (π β π β π½) |
11 | | nconnsubb.5 |
. . . . 5
β’ (π β π β π½) |
12 | | ineq1 4170 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β© π΄) = (π β© π΄)) |
13 | 12 | neeq1d 3004 |
. . . . . . . 8
β’ (π₯ = π β ((π₯ β© π΄) β β
β (π β© π΄) β β
)) |
14 | | ineq1 4170 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ β© π¦) = (π β© π¦)) |
15 | 14 | ineq1d 4176 |
. . . . . . . . 9
β’ (π₯ = π β ((π₯ β© π¦) β© π΄) = ((π β© π¦) β© π΄)) |
16 | 15 | eqeq1d 2739 |
. . . . . . . 8
β’ (π₯ = π β (((π₯ β© π¦) β© π΄) = β
β ((π β© π¦) β© π΄) = β
)) |
17 | 13, 16 | 3anbi13d 1439 |
. . . . . . 7
β’ (π₯ = π β (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π β© π¦) β© π΄) = β
))) |
18 | | uneq1 4121 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ βͺ π¦) = (π βͺ π¦)) |
19 | 18 | ineq1d 4176 |
. . . . . . . 8
β’ (π₯ = π β ((π₯ βͺ π¦) β© π΄) = ((π βͺ π¦) β© π΄)) |
20 | 19 | neeq1d 3004 |
. . . . . . 7
β’ (π₯ = π β (((π₯ βͺ π¦) β© π΄) β π΄ β ((π βͺ π¦) β© π΄) β π΄)) |
21 | 17, 20 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π β ((((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄) β (((π β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π β© π¦) β© π΄) = β
) β ((π βͺ π¦) β© π΄) β π΄))) |
22 | | ineq1 4170 |
. . . . . . . . 9
β’ (π¦ = π β (π¦ β© π΄) = (π β© π΄)) |
23 | 22 | neeq1d 3004 |
. . . . . . . 8
β’ (π¦ = π β ((π¦ β© π΄) β β
β (π β© π΄) β β
)) |
24 | | ineq2 4171 |
. . . . . . . . . 10
β’ (π¦ = π β (π β© π¦) = (π β© π)) |
25 | 24 | ineq1d 4176 |
. . . . . . . . 9
β’ (π¦ = π β ((π β© π¦) β© π΄) = ((π β© π) β© π΄)) |
26 | 25 | eqeq1d 2739 |
. . . . . . . 8
β’ (π¦ = π β (((π β© π¦) β© π΄) = β
β ((π β© π) β© π΄) = β
)) |
27 | 23, 26 | 3anbi23d 1440 |
. . . . . . 7
β’ (π¦ = π β (((π β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π β© π¦) β© π΄) = β
) β ((π β© π΄) β β
β§ (π β© π΄) β β
β§ ((π β© π) β© π΄) = β
))) |
28 | | sseqin2 4180 |
. . . . . . . . 9
β’ (π΄ β (π βͺ π¦) β ((π βͺ π¦) β© π΄) = π΄) |
29 | 28 | necon3bbii 2992 |
. . . . . . . 8
β’ (Β¬
π΄ β (π βͺ π¦) β ((π βͺ π¦) β© π΄) β π΄) |
30 | | uneq2 4122 |
. . . . . . . . . 10
β’ (π¦ = π β (π βͺ π¦) = (π βͺ π)) |
31 | 30 | sseq2d 3981 |
. . . . . . . . 9
β’ (π¦ = π β (π΄ β (π βͺ π¦) β π΄ β (π βͺ π))) |
32 | 31 | notbid 318 |
. . . . . . . 8
β’ (π¦ = π β (Β¬ π΄ β (π βͺ π¦) β Β¬ π΄ β (π βͺ π))) |
33 | 29, 32 | bitr3id 285 |
. . . . . . 7
β’ (π¦ = π β (((π βͺ π¦) β© π΄) β π΄ β Β¬ π΄ β (π βͺ π))) |
34 | 27, 33 | imbi12d 345 |
. . . . . 6
β’ (π¦ = π β ((((π β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π β© π¦) β© π΄) = β
) β ((π βͺ π¦) β© π΄) β π΄) β (((π β© π΄) β β
β§ (π β© π΄) β β
β§ ((π β© π) β© π΄) = β
) β Β¬ π΄ β (π βͺ π)))) |
35 | 21, 34 | rspc2v 3593 |
. . . . 5
β’ ((π β π½ β§ π β π½) β (βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄) β (((π β© π΄) β β
β§ (π β© π΄) β β
β§ ((π β© π) β© π΄) = β
) β Β¬ π΄ β (π βͺ π)))) |
36 | 10, 11, 35 | syl2anc 585 |
. . . 4
β’ (π β (βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄) β (((π β© π΄) β β
β§ (π β© π΄) β β
β§ ((π β© π) β© π΄) = β
) β Β¬ π΄ β (π βͺ π)))) |
37 | 9, 36 | mpid 44 |
. . 3
β’ (π β (βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β
β§ (π¦ β© π΄) β β
β§ ((π₯ β© π¦) β© π΄) = β
) β ((π₯ βͺ π¦) β© π΄) β π΄) β Β¬ π΄ β (π βͺ π))) |
38 | 5, 37 | sylbid 239 |
. 2
β’ (π β ((π½ βΎt π΄) β Conn β Β¬ π΄ β (π βͺ π))) |
39 | 1, 38 | mt2d 136 |
1
β’ (π β Β¬ (π½ βΎt π΄) β Conn) |