This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lhpex2leN

Description: There exist at least two different atoms under a co-atom. This allows 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 ) )