Metamath Proof Explorer

Theorem lhpexle2

Description: There exists atom under a co-atom different from any two other elements. (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpex1.l 
|- .<_ = ( le ` K )
lhpex1.a 
|- A = ( Atoms ` K )
lhpex1.h 
|- H = ( LHyp ` K )
Assertion lhpexle2 
|- ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l 
 |-  .<_ = ( le ` K )
2 lhpex1.a 
 |-  A = ( Atoms ` K )
3 lhpex1.h 
 |-  H = ( LHyp ` K )
4 1 2 3 lhpexle1 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X ) )
5 1 2 3 lhpexle1 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= Y ) )
6 5 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= Y ) )
7 1 2 3 lhpexle2lem 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. A /\ Y .<_ W ) /\ ( X e. A /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= Y /\ p =/= X ) )
8 7 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( X e. A /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= Y /\ p =/= X ) )
9 6 8 lhpexle1lem 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= Y /\ p =/= X ) )
10 3ancomb 
 |-  ( ( p .<_ W /\ p =/= Y /\ p =/= X ) <-> ( p .<_ W /\ p =/= X /\ p =/= Y ) )
11 10 rexbii 
 |-  ( E. p e. A ( p .<_ W /\ p =/= Y /\ p =/= X ) <-> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )
12 9 11 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )
13 4 12 lhpexle1lem 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )