Description: There exists an atom not under a co-atom. (Contributed by NM, 12-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhp2a.l | |
|
lhp2a.a | |
||
lhp2a.h | |
||
Assertion | lhpexnle | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhp2a.l | |
|
2 | lhp2a.a | |
|
3 | lhp2a.h | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 4 5 3 | lhp1cvr | |
7 | simpl | |
|
8 | eqid | |
|
9 | 8 3 | lhpbase | |
10 | 9 | adantl | |
11 | hlop | |
|
12 | 8 4 | op1cl | |
13 | 11 12 | syl | |
14 | 13 | adantr | |
15 | eqid | |
|
16 | 8 1 15 5 2 | cvrval3 | |
17 | 7 10 14 16 | syl3anc | |
18 | 6 17 | mpbid | |
19 | simpl | |
|
20 | 19 | reximi | |
21 | 18 20 | syl | |