Description: Lemma for 4atexlem7 . (Contributed by NM, 23-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | 4thatlem.ph | |- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) ) |
|
| 4thatlem0.l | |- .<_ = ( le ` K ) |
||
| 4thatlem0.j | |- .\/ = ( join ` K ) |
||
| 4thatlem0.m | |- ./\ = ( meet ` K ) |
||
| 4thatlem0.a | |- A = ( Atoms ` K ) |
||
| 4thatlem0.h | |- H = ( LHyp ` K ) |
||
| 4thatlem0.u | |- U = ( ( P .\/ Q ) ./\ W ) |
||
| Assertion | 4atexlemu | |- ( ph -> U e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 4thatlem.ph | |- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) ) |
|
| 2 | 4thatlem0.l | |- .<_ = ( le ` K ) |
|
| 3 | 4thatlem0.j | |- .\/ = ( join ` K ) |
|
| 4 | 4thatlem0.m | |- ./\ = ( meet ` K ) |
|
| 5 | 4thatlem0.a | |- A = ( Atoms ` K ) |
|
| 6 | 4thatlem0.h | |- H = ( LHyp ` K ) |
|
| 7 | 4thatlem0.u | |- U = ( ( P .\/ Q ) ./\ W ) |
|
| 8 | 1 | 4atexlemk | |- ( ph -> K e. HL ) |
| 9 | 1 | 4atexlemw | |- ( ph -> W e. H ) |
| 10 | 1 | 4atexlempw | |- ( ph -> ( P e. A /\ -. P .<_ W ) ) |
| 11 | 1 | 4atexlemq | |- ( ph -> Q e. A ) |
| 12 | 1 | 4atexlempnq | |- ( ph -> P =/= Q ) |
| 13 | 2 3 4 5 6 7 | lhpat2 | |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> U e. A ) |
| 14 | 8 9 10 11 12 13 | syl212anc | |- ( ph -> U e. A ) |