Description: Disconnectedness for a subspace. (Contributed by FL, 29-May-2014) (Proof shortened by Mario Carneiro, 10-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nconnsubb.2 | |
|
nconnsubb.3 | |
||
nconnsubb.4 | |
||
nconnsubb.5 | |
||
nconnsubb.6 | |
||
nconnsubb.7 | |
||
nconnsubb.8 | |
||
nconnsubb.9 | |
||
Assertion | nconnsubb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nconnsubb.2 | |
|
2 | nconnsubb.3 | |
|
3 | nconnsubb.4 | |
|
4 | nconnsubb.5 | |
|
5 | nconnsubb.6 | |
|
6 | nconnsubb.7 | |
|
7 | nconnsubb.8 | |
|
8 | nconnsubb.9 | |
|
9 | connsuba | |
|
10 | 1 2 9 | syl2anc | |
11 | 5 6 7 | 3jca | |
12 | ineq1 | |
|
13 | 12 | neeq1d | |
14 | ineq1 | |
|
15 | 14 | ineq1d | |
16 | 15 | eqeq1d | |
17 | 13 16 | 3anbi13d | |
18 | uneq1 | |
|
19 | 18 | ineq1d | |
20 | 19 | neeq1d | |
21 | 17 20 | imbi12d | |
22 | ineq1 | |
|
23 | 22 | neeq1d | |
24 | ineq2 | |
|
25 | 24 | ineq1d | |
26 | 25 | eqeq1d | |
27 | 23 26 | 3anbi23d | |
28 | sseqin2 | |
|
29 | 28 | necon3bbii | |
30 | uneq2 | |
|
31 | 30 | sseq2d | |
32 | 31 | notbid | |
33 | 29 32 | bitr3id | |
34 | 27 33 | imbi12d | |
35 | 21 34 | rspc2v | |
36 | 3 4 35 | syl2anc | |
37 | 11 36 | mpid | |
38 | 10 37 | sylbid | |
39 | 8 38 | mt2d | |