Description: Create an atom under a co-atom. Part of proof of Lemma B in Crawley p. 112. (Contributed by NM, 21-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhpat.l | |- .<_ = ( le ` K ) |
|
lhpat.j | |- .\/ = ( join ` K ) |
||
lhpat.m | |- ./\ = ( meet ` K ) |
||
lhpat.a | |- A = ( Atoms ` K ) |
||
lhpat.h | |- H = ( LHyp ` K ) |
||
lhpat2.r | |- R = ( ( P .\/ Q ) ./\ W ) |
||
Assertion | lhpat2 | |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> R e. A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpat.l | |- .<_ = ( le ` K ) |
|
2 | lhpat.j | |- .\/ = ( join ` K ) |
|
3 | lhpat.m | |- ./\ = ( meet ` K ) |
|
4 | lhpat.a | |- A = ( Atoms ` K ) |
|
5 | lhpat.h | |- H = ( LHyp ` K ) |
|
6 | lhpat2.r | |- R = ( ( P .\/ Q ) ./\ W ) |
|
7 | 1 2 3 4 5 | lhpat | |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> ( ( P .\/ Q ) ./\ W ) e. A ) |
8 | 6 7 | eqeltrid | |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> R e. A ) |