Step |
Hyp |
Ref |
Expression |
1 |
|
pexmidlem.l |
|- .<_ = ( le ` K ) |
2 |
|
pexmidlem.j |
|- .\/ = ( join ` K ) |
3 |
|
pexmidlem.a |
|- A = ( Atoms ` K ) |
4 |
|
pexmidlem.p |
|- .+ = ( +P ` K ) |
5 |
|
pexmidlem.o |
|- ._|_ = ( _|_P ` K ) |
6 |
|
pexmidlem.m |
|- M = ( X .+ { p } ) |
7 |
|
simpl1 |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> K e. HL ) |
8 |
|
simpl3 |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> p e. A ) |
9 |
8
|
snssd |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> { p } C_ A ) |
10 |
|
simpl2 |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X C_ A ) |
11 |
3 4
|
sspadd2 |
|- ( ( K e. HL /\ { p } C_ A /\ X C_ A ) -> { p } C_ ( X .+ { p } ) ) |
12 |
7 9 10 11
|
syl3anc |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> { p } C_ ( X .+ { p } ) ) |
13 |
|
vex |
|- p e. _V |
14 |
13
|
snss |
|- ( p e. ( X .+ { p } ) <-> { p } C_ ( X .+ { p } ) ) |
15 |
12 14
|
sylibr |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> p e. ( X .+ { p } ) ) |
16 |
15 6
|
eleqtrrdi |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> p e. M ) |
17 |
3 5
|
polssatN |
|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A ) |
18 |
7 10 17
|
syl2anc |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` X ) C_ A ) |
19 |
3 4
|
sspadd1 |
|- ( ( K e. HL /\ X C_ A /\ ( ._|_ ` X ) C_ A ) -> X C_ ( X .+ ( ._|_ ` X ) ) ) |
20 |
7 10 18 19
|
syl3anc |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X C_ ( X .+ ( ._|_ ` X ) ) ) |
21 |
|
simpr3 |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> -. p e. ( X .+ ( ._|_ ` X ) ) ) |
22 |
20 21
|
ssneldd |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> -. p e. X ) |
23 |
|
nelne1 |
|- ( ( p e. M /\ -. p e. X ) -> M =/= X ) |
24 |
16 22 23
|
syl2anc |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M =/= X ) |