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 ) )