Step |
Hyp |
Ref |
Expression |
1 |
|
pexmidALT.a |
|- A = ( Atoms ` K ) |
2 |
|
pexmidALT.p |
|- .+ = ( +P ` K ) |
3 |
|
pexmidALT.o |
|- ._|_ = ( _|_P ` K ) |
4 |
|
nonconne |
|- -. ( X = X /\ X =/= X ) |
5 |
|
simpll |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> K e. HL ) |
6 |
|
simplr |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> X C_ A ) |
7 |
1 3
|
polssatN |
|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A ) |
8 |
7
|
adantr |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( ._|_ ` X ) C_ A ) |
9 |
1 2
|
paddssat |
|- ( ( K e. HL /\ X C_ A /\ ( ._|_ ` X ) C_ A ) -> ( X .+ ( ._|_ ` X ) ) C_ A ) |
10 |
5 6 8 9
|
syl3anc |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) C_ A ) |
11 |
|
df-pss |
|- ( ( X .+ ( ._|_ ` X ) ) C. A <-> ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) ) |
12 |
|
pssnel |
|- ( ( X .+ ( ._|_ ` X ) ) C. A -> E. p ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) |
13 |
11 12
|
sylbir |
|- ( ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) -> E. p ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) |
14 |
|
df-rex |
|- ( E. p e. A -. p e. ( X .+ ( ._|_ ` X ) ) <-> E. p ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) |
15 |
13 14
|
sylibr |
|- ( ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) -> E. p e. A -. p e. ( X .+ ( ._|_ ` X ) ) ) |
16 |
|
simplll |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> K e. HL ) |
17 |
|
simpllr |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X C_ A ) |
18 |
|
simprl |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> p e. A ) |
19 |
|
simplrl |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = X ) |
20 |
|
simplrr |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X =/= (/) ) |
21 |
|
simprr |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> -. p e. ( X .+ ( ._|_ ` X ) ) ) |
22 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
23 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
24 |
|
eqid |
|- ( X .+ { p } ) = ( X .+ { p } ) |
25 |
22 23 1 2 3 24
|
pexmidlem6N |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X .+ { p } ) = X ) |
26 |
22 23 1 2 3 24
|
pexmidlem7N |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X .+ { p } ) =/= X ) |
27 |
25 26
|
jca |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X ) ) |
28 |
16 17 18 19 20 21 27
|
syl33anc |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X ) ) |
29 |
|
nonconne |
|- -. ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X ) |
30 |
29 4
|
2false |
|- ( ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X ) <-> ( X = X /\ X =/= X ) ) |
31 |
28 30
|
sylib |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X = X /\ X =/= X ) ) |
32 |
31
|
rexlimdvaa |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( E. p e. A -. p e. ( X .+ ( ._|_ ` X ) ) -> ( X = X /\ X =/= X ) ) ) |
33 |
15 32
|
syl5 |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) -> ( X = X /\ X =/= X ) ) ) |
34 |
10 33
|
mpand |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( ( X .+ ( ._|_ ` X ) ) =/= A -> ( X = X /\ X =/= X ) ) ) |
35 |
34
|
necon1bd |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( -. ( X = X /\ X =/= X ) -> ( X .+ ( ._|_ ` X ) ) = A ) ) |
36 |
4 35
|
mpi |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) = A ) |