Step | Hyp | Ref
| Expression |
1 | | iunconnlem2.2 |
. 2
β’ (π β π½ β (TopOnβπ)) |
2 | | iunconnlem2.3 |
. . . . 5
β’ ((π β§ π β π΄) β π΅ β π) |
3 | 2 | ex 412 |
. . . 4
β’ (π β (π β π΄ β π΅ β π)) |
4 | 3 | ralrimiv 3137 |
. . 3
β’ (π β βπ β π΄ π΅ β π) |
5 | | iunss 5038 |
. . . 4
β’ (βͺ π β π΄ π΅ β π β βπ β π΄ π΅ β π) |
6 | 5 | biimpri 227 |
. . 3
β’
(βπ β
π΄ π΅ β π β βͺ
π β π΄ π΅ β π) |
7 | 4, 6 | syl 17 |
. 2
β’ (π β βͺ π β π΄ π΅ β π) |
8 | | iunconnlem2.1 |
. . . . . . . . . . . 12
β’ (π β ((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£))) |
9 | 8 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ (π β ((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£))) |
10 | 9 | simprd 495 |
. . . . . . . . . . . . . 14
β’ (π β βͺ π β π΄ π΅ β (π’ βͺ π£)) |
11 | | simp-4r 781 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β (π’ β© βͺ
π β π΄ π΅) β β
) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π’ β© βͺ
π β π΄ π΅) β β
) |
13 | | n0 4338 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π’ β© βͺ π β π΄ π΅) β β
β βπ€ π€ β (π’ β© βͺ
π β π΄ π΅)) |
14 | 13 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β© βͺ π β π΄ π΅) β β
β βπ€ π€ β (π’ β© βͺ
π β π΄ π΅)) |
15 | 12, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ€ π€ β (π’ β© βͺ
π β π΄ π΅)) |
16 | | inss2 4221 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π’ β© βͺ π β π΄ π΅) β βͺ π β π΄ π΅ |
17 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β (π’ β© βͺ
π β π΄ π΅) β π€ β (π’ β© βͺ
π β π΄ π΅)) |
18 | 16, 17 | sselid 3972 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β (π’ β© βͺ
π β π΄ π΅) β π€ β βͺ
π β π΄ π΅) |
19 | | eliun 4991 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β βͺ π β π΄ π΅ β βπ β π΄ π€ β π΅) |
20 | 19 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β βͺ π β π΄ π΅ β βπ β π΄ π€ β π΅) |
21 | 18, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β (π’ β© βͺ
π β π΄ π΅) β βπ β π΄ π€ β π΅) |
22 | | rexn0 4502 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
π΄ π€ β π΅ β π΄ β β
) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β (π’ β© βͺ
π β π΄ π΅) β π΄ β β
) |
24 | 23 | exlimiv 1925 |
. . . . . . . . . . . . . . . . 17
β’
(βπ€ π€ β (π’ β© βͺ
π β π΄ π΅) β π΄ β β
) |
25 | 15, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β β
) |
26 | | nfv 1909 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(π β§ π’ β π½) |
27 | | nfv 1909 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π π£ β π½ |
28 | 26, 27 | nfan 1894 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π((π β§ π’ β π½) β§ π£ β π½) |
29 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²ππ’ |
30 | | nfiu1 5021 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²πβͺ π β π΄ π΅ |
31 | 29, 30 | nfin 4208 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(π’ β© βͺ
π β π΄ π΅) |
32 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²πβ
|
33 | 31, 32 | nfne 3035 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π(π’ β© βͺ π β π΄ π΅) β β
|
34 | 28, 33 | nfan 1894 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) |
35 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²ππ£ |
36 | 35, 30 | nfin 4208 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π(π£ β© βͺ
π β π΄ π΅) |
37 | 36, 32 | nfne 3035 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(π£ β© βͺ π β π΄ π΅) β β
|
38 | 34, 37 | nfan 1894 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) |
39 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(π’ β© π£) |
40 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²ππ |
41 | 40, 30 | nfdif 4117 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(π β βͺ
π β π΄ π΅) |
42 | 39, 41 | nfss 3966 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(π’ β© π£) β (π β βͺ
π β π΄ π΅) |
43 | 38, 42 | nfan 1894 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) |
44 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(π’ βͺ π£) |
45 | 30, 44 | nfss 3966 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβͺ π β π΄ π΅ β (π’ βͺ π£) |
46 | 43, 45 | nfan 1894 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) |
47 | 8 | nfbii 1846 |
. . . . . . . . . . . . . . . . . 18
β’
(β²ππ β β²π((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£))) |
48 | 46, 47 | mpbir 230 |
. . . . . . . . . . . . . . . . 17
β’
β²ππ |
49 | | simp-6l 784 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β π) |
50 | 9, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π) |
51 | | iunconnlem2.4 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π΄) β π β π΅) |
52 | 50, 51 | sylan 579 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π΄) β π β π΅) |
53 | 52 | ex 412 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β π΄ β π β π΅)) |
54 | 48, 53 | ralrimi 3246 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β π΄ π β π΅) |
55 | | r19.2z 4486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β
β§
βπ β π΄ π β π΅) β βπ β π΄ π β π΅) |
56 | 55 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
β’
((βπ β
π΄ π β π΅ β§ π΄ β β
) β βπ β π΄ π β π΅) |
57 | 56 | ancoms 458 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β
β§
βπ β π΄ π β π΅) β βπ β π΄ π β π΅) |
58 | 25, 54, 57 | syl2anc 583 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β π΄ π β π΅) |
59 | | eliun 4991 |
. . . . . . . . . . . . . . . 16
β’ (π β βͺ π β π΄ π΅ β βπ β π΄ π β π΅) |
60 | 59 | biimpri 227 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π΄ π β π΅ β π β βͺ
π β π΄ π΅) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β βͺ
π β π΄ π΅) |
62 | 10, 61 | sseldd 3975 |
. . . . . . . . . . . . 13
β’ (π β π β (π’ βͺ π£)) |
63 | | elun 4140 |
. . . . . . . . . . . . . 14
β’ (π β (π’ βͺ π£) β (π β π’ β¨ π β π£)) |
64 | 63 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β (π’ βͺ π£) β (π β π’ β¨ π β π£)) |
65 | 62, 64 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β π’ β¨ π β π£)) |
66 | 8, 65 | sylbir 234 |
. . . . . . . . . . 11
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β (π β π’ β¨ π β π£)) |
67 | 50, 1 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π½ β (TopOnβπ)) |
68 | 50, 2 | sylan 579 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π΅ β π) |
69 | | iunconnlem2.5 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (π½ βΎt π΅) β Conn) |
70 | 50, 69 | sylan 579 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β (π½ βΎt π΅) β Conn) |
71 | | simp-6r 785 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β π’ β π½) |
72 | 9, 71 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π’ β π½) |
73 | | simp-5r 783 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β π£ β π½) |
74 | 9, 73 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π£ β π½) |
75 | | simpllr 773 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β (π£ β© βͺ
π β π΄ π΅) β β
) |
76 | 9, 75 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π£ β© βͺ
π β π΄ π΅) β β
) |
77 | | simplr 766 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β (π’ β© π£) β (π β βͺ
π β π΄ π΅)) |
78 | 9, 77 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π’ β© π£) β (π β βͺ
π β π΄ π΅)) |
79 | 67, 68, 52, 70, 72, 74, 76, 78, 10, 48 | iunconnlem 23253 |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β π’) |
80 | | incom 4193 |
. . . . . . . . . . . . . . 15
β’ (π£ β© π’) = (π’ β© π£) |
81 | 80, 78 | eqsstrid 4022 |
. . . . . . . . . . . . . 14
β’ (π β (π£ β© π’) β (π β βͺ
π β π΄ π΅)) |
82 | | uncom 4145 |
. . . . . . . . . . . . . . 15
β’ (π£ βͺ π’) = (π’ βͺ π£) |
83 | 10, 82 | sseqtrrdi 4025 |
. . . . . . . . . . . . . 14
β’ (π β βͺ π β π΄ π΅ β (π£ βͺ π’)) |
84 | 67, 68, 52, 70, 74, 72, 12, 81, 83, 48 | iunconnlem 23253 |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β π£) |
85 | | pm4.56 985 |
. . . . . . . . . . . . . . 15
β’ ((Β¬
π β π’ β§ Β¬ π β π£) β Β¬ (π β π’ β¨ π β π£)) |
86 | 85 | biimpi 215 |
. . . . . . . . . . . . . 14
β’ ((Β¬
π β π’ β§ Β¬ π β π£) β Β¬ (π β π’ β¨ π β π£)) |
87 | 86 | idiALT 43727 |
. . . . . . . . . . . . 13
β’ ((Β¬
π β π’ β§ Β¬ π β π£) β Β¬ (π β π’ β¨ π β π£)) |
88 | 79, 84, 87 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (π β Β¬ (π β π’ β¨ π β π£)) |
89 | 8, 88 | sylbir 234 |
. . . . . . . . . . 11
β’
(((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β§ βͺ
π β π΄ π΅ β (π’ βͺ π£)) β Β¬ (π β π’ β¨ π β π£)) |
90 | 66, 89 | pm2.65da 814 |
. . . . . . . . . 10
β’
((((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)) |
91 | 90 | ex 412 |
. . . . . . . . 9
β’
(((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β§ (π£ β© βͺ
π β π΄ π΅) β β
) β ((π’ β© π£) β (π β βͺ
π β π΄ π΅) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))) |
92 | 91 | ex 412 |
. . . . . . . 8
β’ ((((π β§ π’ β π½) β§ π£ β π½) β§ (π’ β© βͺ
π β π΄ π΅) β β
) β ((π£ β© βͺ
π β π΄ π΅) β β
β ((π’ β© π£) β (π β βͺ
π β π΄ π΅) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)))) |
93 | 92 | ex3 1343 |
. . . . . . 7
β’ ((π β§ π’ β π½ β§ π£ β π½) β ((π’ β© βͺ
π β π΄ π΅) β β
β ((π£ β© βͺ
π β π΄ π΅) β β
β ((π’ β© π£) β (π β βͺ
π β π΄ π΅) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))))) |
94 | 93 | 3impd 1345 |
. . . . . 6
β’ ((π β§ π’ β π½ β§ π£ β π½) β (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))) |
95 | 94 | 3expia 1118 |
. . . . 5
β’ ((π β§ π’ β π½) β (π£ β π½ β (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)))) |
96 | 95 | ex 412 |
. . . 4
β’ (π β (π’ β π½ β (π£ β π½ β (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))))) |
97 | 96 | impd 410 |
. . 3
β’ (π β ((π’ β π½ β§ π£ β π½) β (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)))) |
98 | 97 | ralrimivv 3190 |
. 2
β’ (π β βπ’ β π½ βπ£ β π½ (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))) |
99 | | connsub 23247 |
. . 3
β’ ((π½ β (TopOnβπ) β§ βͺ π β π΄ π΅ β π) β ((π½ βΎt βͺ π β π΄ π΅) β Conn β βπ’ β π½ βπ£ β π½ (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£)))) |
100 | 99 | biimp3ar 1466 |
. 2
β’ ((π½ β (TopOnβπ) β§ βͺ π β π΄ π΅ β π β§ βπ’ β π½ βπ£ β π½ (((π’ β© βͺ
π β π΄ π΅) β β
β§ (π£ β© βͺ
π β π΄ π΅) β β
β§ (π’ β© π£) β (π β βͺ
π β π΄ π΅)) β Β¬ βͺ π β π΄ π΅ β (π’ βͺ π£))) β (π½ βΎt βͺ π β π΄ π΅) β Conn) |
101 | 1, 7, 98, 100 | syl3anc 1368 |
1
β’ (π β (π½ βΎt βͺ π β π΄ π΅) β Conn) |