Description: Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 9-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lssat.s | |
|
lssat.a | |
||
Assertion | lssat | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lssat.s | |
|
2 | lssat.a | |
|
3 | dfpss3 | |
|
4 | 3 | simprbi | |
5 | ss2rab | |
|
6 | iman | |
|
7 | 6 | ralbii | |
8 | 5 7 | bitr2i | |
9 | simpl1 | |
|
10 | 1 2 | lsatlss | |
11 | rabss2 | |
|
12 | uniss | |
|
13 | 9 10 11 12 | 4syl | |
14 | simpl2 | |
|
15 | unimax | |
|
16 | 14 15 | syl | |
17 | eqid | |
|
18 | 17 1 | lssss | |
19 | 14 18 | syl | |
20 | 16 19 | eqsstrd | |
21 | 13 20 | sstrd | |
22 | uniss | |
|
23 | 22 | adantl | |
24 | eqid | |
|
25 | 17 24 | lspss | |
26 | 9 21 23 25 | syl3anc | |
27 | simpl3 | |
|
28 | 1 24 2 | lssats | |
29 | 9 27 28 | syl2anc | |
30 | 1 24 2 | lssats | |
31 | 9 14 30 | syl2anc | |
32 | 26 29 31 | 3sstr4d | |
33 | 32 | ex | |
34 | 8 33 | syl5bi | |
35 | 34 | con3dimp | |
36 | dfrex2 | |
|
37 | 35 36 | sylibr | |
38 | 4 37 | sylan2 | |