Metamath Proof Explorer


Theorem lhpex2leN

Description: There exist at least two different atoms under a co-atom. This allows us to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lhp2at.l
 |-  .<_ = ( le ` K )
2 lhp2at.a
 |-  A = ( Atoms ` K )
3 lhp2at.h
 |-  H = ( LHyp ` K )
4 simprr
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ p .<_ W ) ) -> p .<_ W )
5 1 2 3 lhpexle1
 |-  ( ( K e. HL /\ W e. H ) -> E. q e. A ( q .<_ W /\ q =/= p ) )
6 5 adantr
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ p .<_ W ) ) -> E. q e. A ( q .<_ W /\ q =/= p ) )
7 4 6 jca
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ p .<_ W ) ) -> ( p .<_ W /\ E. q e. A ( q .<_ W /\ q =/= p ) ) )
8 necom
 |-  ( p =/= q <-> q =/= p )
9 8 3anbi3i
 |-  ( ( p .<_ W /\ q .<_ W /\ p =/= q ) <-> ( p .<_ W /\ q .<_ W /\ q =/= p ) )
10 3anass
 |-  ( ( p .<_ W /\ q .<_ W /\ q =/= p ) <-> ( p .<_ W /\ ( q .<_ W /\ q =/= p ) ) )
11 9 10 bitri
 |-  ( ( p .<_ W /\ q .<_ W /\ p =/= q ) <-> ( p .<_ W /\ ( q .<_ W /\ q =/= p ) ) )
12 11 rexbii
 |-  ( E. q e. A ( p .<_ W /\ q .<_ W /\ p =/= q ) <-> E. q e. A ( p .<_ W /\ ( q .<_ W /\ q =/= p ) ) )
13 r19.42v
 |-  ( E. q e. A ( p .<_ W /\ ( q .<_ W /\ q =/= p ) ) <-> ( p .<_ W /\ E. q e. A ( q .<_ W /\ q =/= p ) ) )
14 12 13 bitr2i
 |-  ( ( p .<_ W /\ E. q e. A ( q .<_ W /\ q =/= p ) ) <-> E. q e. A ( p .<_ W /\ q .<_ W /\ p =/= q ) )
15 7 14 sylib
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ p .<_ W ) ) -> E. q e. A ( p .<_ W /\ q .<_ W /\ p =/= q ) )
16 1 2 3 lhpexle
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A p .<_ W )
17 15 16 reximddv
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A E. q e. A ( p .<_ W /\ q .<_ W /\ p =/= q ) )