Step | Hyp | Ref
| Expression |
1 | | df-3an 1089 |
. . . 4
β’ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β ((π₯ β β
β§ π¦ β β
) β§ (π₯ β© π¦) = β
)) |
2 | | n0 4346 |
. . . . . . . 8
β’ (π₯ β β
β
βπ π β π₯) |
3 | | n0 4346 |
. . . . . . . 8
β’ (π¦ β β
β
βπ π β π¦) |
4 | 2, 3 | anbi12i 627 |
. . . . . . 7
β’ ((π₯ β β
β§ π¦ β β
) β
(βπ π β π₯ β§ βπ π β π¦)) |
5 | | exdistrv 1959 |
. . . . . . 7
β’
(βπβπ(π β π₯ β§ π β π¦) β (βπ π β π₯ β§ βπ π β π¦)) |
6 | 4, 5 | bitr4i 277 |
. . . . . 6
β’ ((π₯ β β
β§ π¦ β β
) β
βπβπ(π β π₯ β§ π β π¦)) |
7 | | simpll 765 |
. . . . . . . . . 10
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β π½ β PConn) |
8 | | simprll 777 |
. . . . . . . . . . 11
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β π β π₯) |
9 | | simplrl 775 |
. . . . . . . . . . 11
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β π₯ β π½) |
10 | | elunii 4913 |
. . . . . . . . . . 11
β’ ((π β π₯ β§ π₯ β π½) β π β βͺ π½) |
11 | 8, 9, 10 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β π β βͺ π½) |
12 | | simprlr 778 |
. . . . . . . . . . 11
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β π β π¦) |
13 | | simplrr 776 |
. . . . . . . . . . 11
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β π¦ β π½) |
14 | | elunii 4913 |
. . . . . . . . . . 11
β’ ((π β π¦ β§ π¦ β π½) β π β βͺ π½) |
15 | 12, 13, 14 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β π β βͺ π½) |
16 | | eqid 2732 |
. . . . . . . . . . 11
β’ βͺ π½ =
βͺ π½ |
17 | 16 | pconncn 34284 |
. . . . . . . . . 10
β’ ((π½ β PConn β§ π β βͺ π½
β§ π β βͺ π½)
β βπ β (II
Cn π½)((πβ0) = π β§ (πβ1) = π)) |
18 | 7, 11, 15, 17 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β βπ β (II Cn π½)((πβ0) = π β§ (πβ1) = π)) |
19 | | simplrr 776 |
. . . . . . . . . . . . 13
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (π₯ β© π¦) = β
) |
20 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
β’ (((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½) β (πβ1) = π) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (πβ1) = π) |
22 | | iiuni 24404 |
. . . . . . . . . . . . . . . . 17
β’ (0[,]1) =
βͺ II |
23 | | iiconn 24410 |
. . . . . . . . . . . . . . . . . 18
β’ II β
Conn |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β II β
Conn) |
25 | | simprll 777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π β (II Cn π½)) |
26 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π₯ β π½) |
27 | | uncom 4153 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ βͺ π₯) = (π₯ βͺ π¦) |
28 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (π₯ βͺ π¦) = βͺ π½) |
29 | 27, 28 | eqtrid 2784 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (π¦ βͺ π₯) = βͺ π½) |
30 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π¦ β π½) |
31 | | elssuni 4941 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β π½ β π¦ β βͺ π½) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π¦ β βͺ π½) |
33 | | incom 4201 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β© π₯) = (π₯ β© π¦) |
34 | 33, 19 | eqtrid 2784 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (π¦ β© π₯) = β
) |
35 | | uneqdifeq 4492 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β βͺ π½
β§ (π¦ β© π₯) = β
) β ((π¦ βͺ π₯) = βͺ π½ β (βͺ π½
β π¦) = π₯)) |
36 | 32, 34, 35 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β ((π¦ βͺ π₯) = βͺ π½ β (βͺ π½
β π¦) = π₯)) |
37 | 29, 36 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (βͺ π½
β π¦) = π₯) |
38 | | pconntop 34285 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π½ β PConn β π½ β Top) |
39 | 38 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π½ β Top) |
40 | 16 | opncld 22544 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π½ β Top β§ π¦ β π½) β (βͺ π½ β π¦) β (Clsdβπ½)) |
41 | 39, 30, 40 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (βͺ π½
β π¦) β
(Clsdβπ½)) |
42 | 37, 41 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π₯ β (Clsdβπ½)) |
43 | | 0elunit 13448 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
(0[,]1) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β 0 β
(0[,]1)) |
45 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½) β (πβ0) = π) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (πβ0) = π) |
47 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π β π₯) |
48 | 46, 47 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (πβ0) β π₯) |
49 | 22, 24, 25, 26, 42, 44, 48 | conncn 22937 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π:(0[,]1)βΆπ₯) |
50 | | 1elunit 13449 |
. . . . . . . . . . . . . . . 16
β’ 1 β
(0[,]1) |
51 | | ffvelcdm 7083 |
. . . . . . . . . . . . . . . 16
β’ ((π:(0[,]1)βΆπ₯ β§ 1 β (0[,]1)) β
(πβ1) β π₯) |
52 | 49, 50, 51 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (πβ1) β π₯) |
53 | 21, 52 | eqeltrrd 2834 |
. . . . . . . . . . . . . 14
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π β π₯) |
54 | 12 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β π β π¦) |
55 | | inelcm 4464 |
. . . . . . . . . . . . . 14
β’ ((π β π₯ β§ π β π¦) β (π₯ β© π¦) β β
) |
56 | 53, 54, 55 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β (π₯ β© π¦) β β
) |
57 | 19, 56 | pm2.21ddne 3026 |
. . . . . . . . . . . 12
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ ((π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π)) β§ (π₯ βͺ π¦) = βͺ π½)) β Β¬ (π₯ βͺ π¦) = βͺ π½) |
58 | 57 | expr 457 |
. . . . . . . . . . 11
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ (π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π))) β ((π₯ βͺ π¦) = βͺ π½ β Β¬ (π₯ βͺ π¦) = βͺ π½)) |
59 | 58 | pm2.01d 189 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ (π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π))) β Β¬ (π₯ βͺ π¦) = βͺ π½) |
60 | 59 | neqned 2947 |
. . . . . . . . 9
β’ ((((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β§ (π β (II Cn π½) β§ ((πβ0) = π β§ (πβ1) = π))) β (π₯ βͺ π¦) β βͺ π½) |
61 | 18, 60 | rexlimddv 3161 |
. . . . . . . 8
β’ (((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β§ ((π β π₯ β§ π β π¦) β§ (π₯ β© π¦) = β
)) β (π₯ βͺ π¦) β βͺ π½) |
62 | 61 | exp32 421 |
. . . . . . 7
β’ ((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β ((π β π₯ β§ π β π¦) β ((π₯ β© π¦) = β
β (π₯ βͺ π¦) β βͺ π½))) |
63 | 62 | exlimdvv 1937 |
. . . . . 6
β’ ((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β (βπβπ(π β π₯ β§ π β π¦) β ((π₯ β© π¦) = β
β (π₯ βͺ π¦) β βͺ π½))) |
64 | 6, 63 | biimtrid 241 |
. . . . 5
β’ ((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β ((π₯ β β
β§ π¦ β β
) β ((π₯ β© π¦) = β
β (π₯ βͺ π¦) β βͺ π½))) |
65 | 64 | impd 411 |
. . . 4
β’ ((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β (((π₯ β β
β§ π¦ β β
) β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) |
66 | 1, 65 | biimtrid 241 |
. . 3
β’ ((π½ β PConn β§ (π₯ β π½ β§ π¦ β π½)) β ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) |
67 | 66 | ralrimivva 3200 |
. 2
β’ (π½ β PConn β
βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) |
68 | 16 | toptopon 22426 |
. . . 4
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
69 | 38, 68 | sylib 217 |
. . 3
β’ (π½ β PConn β π½ β (TopOnββͺ π½)) |
70 | | dfconn2 22930 |
. . 3
β’ (π½ β (TopOnββͺ π½)
β (π½ β Conn
β βπ₯ β
π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½))) |
71 | 69, 70 | syl 17 |
. 2
β’ (π½ β PConn β (π½ β Conn β
βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½))) |
72 | 67, 71 | mpbird 256 |
1
β’ (π½ β PConn β π½ β Conn) |