Metamath Proof Explorer

Theorem pexmidlem4N

Description: Lemma for pexmidN . (Contributed by NM, 2-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmidlem.l 
|- .<_ = ( le ` K )
pexmidlem.j 
|- .\/ = ( join ` K )
pexmidlem.a 
|- A = ( Atoms ` K )
pexmidlem.p 
|- .+ = ( +P ` K )
pexmidlem.o 
|- ._|_ = ( _|_P ` K )
pexmidlem.m 
|- M = ( X .+ { p } )
Assertion pexmidlem4N 
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )

Proof

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 =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> K e. HL )
8 7 hllatd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> K e. Lat )
9 simpl2 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> X C_ A )
10 simpl3 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> p e. A )
11 simprl 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> X =/= (/) )
12 inss2 
 |-  ( ( ._|_ ` X ) i^i M ) C_ M
13 12 sseli 
 |-  ( q e. ( ( ._|_ ` X ) i^i M ) -> q e. M )
14 13 6 eleqtrdi 
 |-  ( q e. ( ( ._|_ ` X ) i^i M ) -> q e. ( X .+ { p } ) )
15 14 ad2antll 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> q e. ( X .+ { p } ) )
16 1 2 3 4 elpaddatiN 
 |-  ( ( ( K e. Lat /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( X .+ { p } ) ) ) -> E. r e. X q .<_ ( r .\/ p ) )
17 8 9 10 11 15 16 syl32anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> E. r e. X q .<_ ( r .\/ p ) )
18 simp1 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) /\ ( r e. X /\ q .<_ ( r .\/ p ) ) ) -> ( K e. HL /\ X C_ A /\ p e. A ) )
19 simp3l 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) /\ ( r e. X /\ q .<_ ( r .\/ p ) ) ) -> r e. X )
20 inss1 
 |-  ( ( ._|_ ` X ) i^i M ) C_ ( ._|_ ` X )
21 simp2r 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) /\ ( r e. X /\ q .<_ ( r .\/ p ) ) ) -> q e. ( ( ._|_ ` X ) i^i M ) )
22 20 21 sselid 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) /\ ( r e. X /\ q .<_ ( r .\/ p ) ) ) -> q e. ( ._|_ ` X ) )
23 simp3r 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) /\ ( r e. X /\ q .<_ ( r .\/ p ) ) ) -> q .<_ ( r .\/ p ) )
24 1 2 3 4 5 6 pexmidlem3N 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )
25 18 19 22 23 24 syl121anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) /\ ( r e. X /\ q .<_ ( r .\/ p ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )
26 25 3expia 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> ( ( r e. X /\ q .<_ ( r .\/ p ) ) -> p e. ( X .+ ( ._|_ ` X ) ) ) )
27 26 expd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> ( r e. X -> ( q .<_ ( r .\/ p ) -> p e. ( X .+ ( ._|_ ` X ) ) ) ) )
28 27 rexlimdv 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> ( E. r e. X q .<_ ( r .\/ p ) -> p e. ( X .+ ( ._|_ ` X ) ) ) )
29 17 28 mpd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )