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 |
|
n0i |
|- ( r e. ( X i^i ( ._|_ ` X ) ) -> -. ( X i^i ( ._|_ ` X ) ) = (/) ) |
8 |
3 5
|
pnonsingN |
|- ( ( K e. HL /\ X C_ A ) -> ( X i^i ( ._|_ ` X ) ) = (/) ) |
9 |
8
|
adantr |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> ( X i^i ( ._|_ ` X ) ) = (/) ) |
10 |
7 9
|
nsyl3 |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> -. r e. ( X i^i ( ._|_ ` X ) ) ) |
11 |
|
simprr |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> q e. ( ._|_ ` X ) ) |
12 |
|
eleq1w |
|- ( q = r -> ( q e. ( ._|_ ` X ) <-> r e. ( ._|_ ` X ) ) ) |
13 |
11 12
|
syl5ibcom |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> ( q = r -> r e. ( ._|_ ` X ) ) ) |
14 |
|
simprl |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> r e. X ) |
15 |
13 14
|
jctild |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> ( q = r -> ( r e. X /\ r e. ( ._|_ ` X ) ) ) ) |
16 |
|
elin |
|- ( r e. ( X i^i ( ._|_ ` X ) ) <-> ( r e. X /\ r e. ( ._|_ ` X ) ) ) |
17 |
15 16
|
syl6ibr |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> ( q = r -> r e. ( X i^i ( ._|_ ` X ) ) ) ) |
18 |
17
|
necon3bd |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> ( -. r e. ( X i^i ( ._|_ ` X ) ) -> q =/= r ) ) |
19 |
10 18
|
mpd |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> q =/= r ) |