Description: The orthocomplement of an element covered by 1 is an atom. (Contributed by NM, 7-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 1cvrco.b | |
|
1cvrco.u | |
||
1cvrco.o | |
||
1cvrco.c | |
||
1cvrco.a | |
||
Assertion | 1cvrco | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1cvrco.b | |
|
2 | 1cvrco.u | |
|
3 | 1cvrco.o | |
|
4 | 1cvrco.c | |
|
5 | 1cvrco.a | |
|
6 | hlop | |
|
7 | 6 | adantr | |
8 | simpr | |
|
9 | 1 2 | op1cl | |
10 | 7 9 | syl | |
11 | 1 3 4 | cvrcon3b | |
12 | 7 8 10 11 | syl3anc | |
13 | eqid | |
|
14 | 13 2 3 | opoc1 | |
15 | 7 14 | syl | |
16 | 15 | breq1d | |
17 | 1 3 | opoccl | |
18 | 6 17 | sylan | |
19 | 18 | biantrurd | |
20 | 12 16 19 | 3bitrd | |
21 | 1 13 4 5 | isat | |
22 | 21 | adantr | |
23 | 20 22 | bitr4d | |