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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lhp2at.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lhp2at.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpex2leN	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists p\in A\exists q\in A\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge p\ne q\right)$$

Proof

Step	Hyp	Ref	Expression
1		lhp2at.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lhp2at.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		lhp2at.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		simprr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(p\in A\wedge p\underset{\dot{}}{\le }W\right)\right)\to p\underset{\dot{}}{\le }W$$
5	1 2 3	lhpexle1	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists q\in A\left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)$$
6	5	adantr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(p\in A\wedge p\underset{\dot{}}{\le }W\right)\right)\to \exists q\in A\left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)$$
7	4 6	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(p\in A\wedge p\underset{\dot{}}{\le }W\right)\right)\to \left(p\underset{\dot{}}{\le }W\wedge \exists q\in A\left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)\right)$$
8		necom	$$⊢p\ne q\leftrightarrow q\ne p$$
9	8	3anbi3i	$$⊢\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge p\ne q\right)\leftrightarrow \left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge q\ne p\right)$$
10		3anass	$$⊢\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge q\ne p\right)\leftrightarrow \left(p\underset{\dot{}}{\le }W\wedge \left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)\right)$$
11	9 10	bitri	$$⊢\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge p\ne q\right)\leftrightarrow \left(p\underset{\dot{}}{\le }W\wedge \left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)\right)$$
12	11	rexbii	$$⊢\exists q\in A\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge p\ne q\right)\leftrightarrow \exists q\in A\left(p\underset{\dot{}}{\le }W\wedge \left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)\right)$$
13		r19.42v	$$⊢\exists q\in A\left(p\underset{\dot{}}{\le }W\wedge \left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\le }W\wedge \exists q\in A\left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)\right)$$
14	12 13	bitr2i	$$⊢\left(p\underset{\dot{}}{\le }W\wedge \exists q\in A\left(q\underset{\dot{}}{\le }W\wedge q\ne p\right)\right)\leftrightarrow \exists q\in A\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge p\ne q\right)$$
15	7 14	sylib	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(p\in A\wedge p\underset{\dot{}}{\le }W\right)\right)\to \exists q\in A\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge p\ne q\right)$$
16	1 2 3	lhpexle	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists p\in Ap\underset{\dot{}}{\le }W$$
17	15 16	reximddv	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists p\in A\exists q\in A\left(p\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\le }W\wedge p\ne q\right)$$