Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β βͺ
π β π΄ π΅ β (π’ βͺ π£)) |
2 | | simplr1 1216 |
. . . . . . . . . 10
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β (π’ β© βͺ
π β π΄ π΅) β β
) |
3 | | n0 4310 |
. . . . . . . . . . 11
β’ ((π’ β© βͺ π β π΄ π΅) β β
β βπ£ π£ β (π’ β© βͺ
π β π΄ π΅)) |
4 | | elinel2 4160 |
. . . . . . . . . . . . 13
β’ (π£ β (π’ β© βͺ
π β π΄ π΅) β π£ β βͺ
π β π΄ π΅) |
5 | | eliun 4962 |
. . . . . . . . . . . . . 14
β’ (π£ β βͺ π β π΄ π΅ β βπ β π΄ π£ β π΅) |
6 | | rexn0 4472 |
. . . . . . . . . . . . . 14
β’
(βπ β
π΄ π£ β π΅ β π΄ β β
) |
7 | 5, 6 | sylbi 216 |
. . . . . . . . . . . . 13
β’ (π£ β βͺ π β π΄ π΅ β π΄ β β
) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . . 12
β’ (π£ β (π’ β© βͺ
π β π΄ π΅) β π΄ β β
) |
9 | 8 | exlimiv 1934 |
. . . . . . . . . . 11
β’
(βπ£ π£ β (π’ β© βͺ
π β π΄ π΅) β π΄ β β
) |
10 | 3, 9 | sylbi 216 |
. . . . . . . . . 10
β’ ((π’ β© βͺ π β π΄ π΅) β β
β π΄ β β
) |
11 | 2, 10 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β π΄ β β
) |
12 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β π) |
13 | | iunconn.4 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β π β π΅) |
14 | 13 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (π β βπ β π΄ π β π΅) |
15 | 12, 14 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β βπ β π΄ π β π΅) |
16 | | r19.2z 4456 |
. . . . . . . . 9
β’ ((π΄ β β
β§
βπ β π΄ π β π΅) β βπ β π΄ π β π΅) |
17 | 11, 15, 16 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β βπ β π΄ π β π΅) |
18 | | eliun 4962 |
. . . . . . . 8
β’ (π β βͺ π β π΄ π΅ β βπ β π΄ π β π΅) |
19 | 17, 18 | sylibr 233 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β π β βͺ
π β π΄ π΅) |
20 | 1, 19 | sseldd 3949 |
. . . . . 6
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β π β (π’ βͺ π£)) |
21 | | elun 4112 |
. . . . . 6
β’ (π β (π’ βͺ π£) β (π β π’ β¨ π β π£)) |
22 | 20, 21 | sylib 217 |
. . . . 5
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β (π β π’ β¨ π β π£)) |
23 | | iunconn.2 |
. . . . . . . 8
β’ (π β π½ β (TopOnβπ)) |
24 | 12, 23 | syl 17 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β π½ β (TopOnβπ)) |
25 | | iunconn.3 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π΅ β π) |
26 | 12, 25 | sylan 581 |
. . . . . . 7
β’
(((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β§ π β π΄) β π΅ β π) |
27 | 12, 13 | sylan 581 |
. . . . . . 7
β’
(((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β§ π β π΄) β π β π΅) |
28 | | iunconn.5 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (π½ βΎt π΅) β Conn) |
29 | 12, 28 | sylan 581 |
. . . . . . 7
β’
(((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β§ π β π΄) β (π½ βΎt π΅) β Conn) |
30 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β (π’ β π½ β§ π£ β π½)) |
31 | 30 | simpld 496 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β π’ β π½) |
32 | 30 | simprd 497 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β π£ β π½) |
33 | | simplr2 1217 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β (π£ β© βͺ
π β π΄ π΅) β β
) |
34 | | simplr3 1218 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β (π’ β© π£) β (π β βͺ
π β π΄ π΅)) |
35 | | nfv 1918 |
. . . . . . . . 9
β’
β²π(π β§ (π’ β π½ β§ π£ β π½)) |
36 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ππ’ |
37 | | nfiu1 4992 |
. . . . . . . . . . . 12
β’
β²πβͺ π β π΄ π΅ |
38 | 36, 37 | nfin 4180 |
. . . . . . . . . . 11
β’
β²π(π’ β© βͺ
π β π΄ π΅) |
39 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²πβ
|
40 | 38, 39 | nfne 3042 |
. . . . . . . . . 10
β’
β²π(π’ β© βͺ π β π΄ π΅) β β
|
41 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ππ£ |
42 | 41, 37 | nfin 4180 |
. . . . . . . . . . 11
β’
β²π(π£ β© βͺ
π β π΄ π΅) |
43 | 42, 39 | nfne 3042 |
. . . . . . . . . 10
β’
β²π(π£ β© βͺ π β π΄ π΅) β β
|
44 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π(π’ β© π£) |
45 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ππ |
46 | 45, 37 | nfdif 4089 |
. . . . . . . . . . 11
β’
β²π(π β βͺ
π β π΄ π΅) |
47 | 44, 46 | nfss 3940 |
. . . . . . . . . 10
β’
β²π(π’ β© π£) β (π β βͺ
π β π΄ π΅) |
48 | 40, 43, 47 | nf3an 1905 |
. . . . . . . . 9
β’
β²π((π’ β© βͺ π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) |
49 | 35, 48 | nfan 1903 |
. . . . . . . 8
β’
β²π((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) |
50 | 36, 41 | nfun 4129 |
. . . . . . . . 9
β’
β²π(π’ βͺ π£) |
51 | 37, 50 | nfss 3940 |
. . . . . . . 8
β’
β²πβͺ π β π΄ π΅ β (π’ βͺ π£) |
52 | 49, 51 | nfan 1903 |
. . . . . . 7
β’
β²π(((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) |
53 | 24, 26, 27, 29, 31, 32, 33, 34, 1, 52 | iunconnlem 22801 |
. . . . . 6
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β Β¬ π β π’) |
54 | | incom 4165 |
. . . . . . . 8
β’ (π£ β© π’) = (π’ β© π£) |
55 | 54, 34 | eqsstrid 3996 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β (π£ β© π’) β (π β βͺ
π β π΄ π΅)) |
56 | | uncom 4117 |
. . . . . . . 8
β’ (π’ βͺ π£) = (π£ βͺ π’) |
57 | 1, 56 | sseqtrdi 3998 |
. . . . . . 7
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β βͺ
π β π΄ π΅ β (π£ βͺ π’)) |
58 | 24, 26, 27, 29, 32, 31, 2, 55, 57, 52 | iunconnlem 22801 |
. . . . . 6
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β Β¬ π β π£) |
59 | | ioran 983 |
. . . . . 6
β’ (Β¬
(π β π’ β¨ π β π£) β (Β¬ π β π’ β§ Β¬ π β π£)) |
60 | 53, 58, 59 | sylanbrc 584 |
. . . . 5
β’ ((((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β§ βͺ π β π΄ π΅ β (π’ βͺ π£)) β Β¬ (π β π’ β¨ π β π£)) |
61 | 22, 60 | pm2.65da 816 |
. . . 4
β’ (((π β§ (π’ β π½ β§ π£ β π½)) β§ ((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅))) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)) |
62 | 61 | ex 414 |
. . 3
β’ ((π β§ (π’ β π½ β§ π£ β π½)) β (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))) |
63 | 62 | ralrimivva 3194 |
. 2
β’ (π β βπ’ β π½ βπ£ β π½ (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))) |
64 | 25 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β π΄ π΅ β π) |
65 | | iunss 5009 |
. . . 4
β’ (βͺ π β π΄ π΅ β π β βπ β π΄ π΅ β π) |
66 | 64, 65 | sylibr 233 |
. . 3
β’ (π β βͺ π β π΄ π΅ β π) |
67 | | connsub 22795 |
. . 3
β’ ((π½ β (TopOnβπ) β§ βͺ π β π΄ π΅ β π) β ((π½ βΎt βͺ π β π΄ π΅) β Conn β βπ’ β π½ βπ£ β π½ (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)))) |
68 | 23, 66, 67 | syl2anc 585 |
. 2
β’ (π β ((π½ βΎt βͺ π β π΄ π΅) β Conn β βπ’ β π½ βπ£ β π½ (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)))) |
69 | 63, 68 | mpbird 257 |
1
β’ (π β (π½ βΎt βͺ π β π΄ π΅) β Conn) |