Description: A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lssats2.s | |
|
lssats2.n | |
||
lssats2.w | |
||
lssats2.u | |
||
Assertion | lssats2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lssats2.s | |
|
2 | lssats2.n | |
|
3 | lssats2.w | |
|
4 | lssats2.u | |
|
5 | simpr | |
|
6 | 3 | adantr | |
7 | eqid | |
|
8 | 7 1 | lssel | |
9 | 4 8 | sylan | |
10 | 7 2 | lspsnid | |
11 | 6 9 10 | syl2anc | |
12 | sneq | |
|
13 | 12 | fveq2d | |
14 | 13 | eleq2d | |
15 | 14 | rspcev | |
16 | 5 11 15 | syl2anc | |
17 | 16 | ex | |
18 | 3 | adantr | |
19 | 4 | adantr | |
20 | simpr | |
|
21 | 1 2 18 19 20 | lspsnel5a | |
22 | 21 | sseld | |
23 | 22 | rexlimdva | |
24 | 17 23 | impbid | |
25 | eliun | |
|
26 | 24 25 | bitr4di | |
27 | 26 | eqrdv | |