Step | Hyp | Ref
| Expression |
1 | | iunconn.8 |
. . 3
β’ (π β (π β© βͺ
π β π΄ π΅) β β
) |
2 | | n0 4310 |
. . 3
β’ ((π β© βͺ π β π΄ π΅) β β
β βπ₯ π₯ β (π β© βͺ
π β π΄ π΅)) |
3 | 1, 2 | sylib 217 |
. 2
β’ (π β βπ₯ π₯ β (π β© βͺ
π β π΄ π΅)) |
4 | | elin 3930 |
. . . 4
β’ (π₯ β (π β© βͺ
π β π΄ π΅) β (π₯ β π β§ π₯ β βͺ
π β π΄ π΅)) |
5 | | eliun 4962 |
. . . . . 6
β’ (π₯ β βͺ π β π΄ π΅ β βπ β π΄ π₯ β π΅) |
6 | | iunconn.11 |
. . . . . . . 8
β’
β²ππ |
7 | | nfv 1918 |
. . . . . . . 8
β’
β²π π₯ β π |
8 | 6, 7 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ π₯ β π) |
9 | | nfv 1918 |
. . . . . . 7
β’
β²π Β¬ π β π |
10 | | iunconn.5 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (π½ βΎt π΅) β Conn) |
11 | 10 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ (π₯ β π β§ π₯ β π΅)) β (π½ βΎt π΅) β Conn) |
12 | | iunconn.2 |
. . . . . . . . . . . . 13
β’ (π β π½ β (TopOnβπ)) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π½ β (TopOnβπ)) |
14 | | iunconn.3 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β π΅ β π) |
15 | 14 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π΅ β π) |
16 | | iunconn.6 |
. . . . . . . . . . . . 13
β’ (π β π β π½) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π β π½) |
18 | | iunconn.7 |
. . . . . . . . . . . . 13
β’ (π β π β π½) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π β π½) |
20 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π β π) |
21 | | iunconn.4 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π β π΅) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π β π΅) |
23 | | inelcm 4428 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π΅) β (π β© π΅) β β
) |
24 | 20, 22, 23 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β (π β© π΅) β β
) |
25 | | inelcm 4428 |
. . . . . . . . . . . . 13
β’ ((π₯ β π β§ π₯ β π΅) β (π β© π΅) β β
) |
26 | 25 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β (π β© π΅) β β
) |
27 | | iunconn.9 |
. . . . . . . . . . . . . . 15
β’ (π β (π β© π) β (π β βͺ
π β π΄ π΅)) |
28 | 27 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β (π β© π) β (π β βͺ
π β π΄ π΅)) |
29 | | ssiun2 5011 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β π΅ β βͺ
π β π΄ π΅) |
30 | 29 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π΅ β βͺ
π β π΄ π΅) |
31 | 30 | sscond 4105 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β (π β βͺ
π β π΄ π΅) β (π β π΅)) |
32 | 28, 31 | sstrd 3958 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β (π β© π) β (π β π΅)) |
33 | | inss1 4192 |
. . . . . . . . . . . . . . 15
β’ (π β© π) β π |
34 | | toponss 22299 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ π β π½) β π β π) |
35 | 13, 17, 34 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π β π) |
36 | 33, 35 | sstrid 3959 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β (π β© π) β π) |
37 | | reldisj 4415 |
. . . . . . . . . . . . . 14
β’ ((π β© π) β π β (((π β© π) β© π΅) = β
β (π β© π) β (π β π΅))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β (((π β© π) β© π΅) = β
β (π β© π) β (π β π΅))) |
39 | 32, 38 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β ((π β© π) β© π΅) = β
) |
40 | | iunconn.10 |
. . . . . . . . . . . . . 14
β’ (π β βͺ π β π΄ π΅ β (π βͺ π)) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β βͺ π β π΄ π΅ β (π βͺ π)) |
42 | 30, 41 | sstrd 3958 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β π΅ β (π βͺ π)) |
43 | 13, 15, 17, 19, 24, 26, 39, 42 | nconnsubb 22797 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ ((π₯ β π β§ π₯ β π΅) β§ π β π)) β Β¬ (π½ βΎt π΅) β Conn) |
44 | 43 | expr 458 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ (π₯ β π β§ π₯ β π΅)) β (π β π β Β¬ (π½ βΎt π΅) β Conn)) |
45 | 11, 44 | mt2d 136 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ (π₯ β π β§ π₯ β π΅)) β Β¬ π β π) |
46 | 45 | an4s 659 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β π΄ β§ π₯ β π΅)) β Β¬ π β π) |
47 | 46 | exp32 422 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π β π΄ β (π₯ β π΅ β Β¬ π β π))) |
48 | 8, 9, 47 | rexlimd 3248 |
. . . . . 6
β’ ((π β§ π₯ β π) β (βπ β π΄ π₯ β π΅ β Β¬ π β π)) |
49 | 5, 48 | biimtrid 241 |
. . . . 5
β’ ((π β§ π₯ β π) β (π₯ β βͺ
π β π΄ π΅ β Β¬ π β π)) |
50 | 49 | expimpd 455 |
. . . 4
β’ (π β ((π₯ β π β§ π₯ β βͺ
π β π΄ π΅) β Β¬ π β π)) |
51 | 4, 50 | biimtrid 241 |
. . 3
β’ (π β (π₯ β (π β© βͺ
π β π΄ π΅) β Β¬ π β π)) |
52 | 51 | exlimdv 1937 |
. 2
β’ (π β (βπ₯ π₯ β (π β© βͺ
π β π΄ π΅) β Β¬ π β π)) |
53 | 3, 52 | mpd 15 |
1
β’ (π β Β¬ π β π) |