Theorem lhpocnel2

Description: The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014)

	Ref	Expression
Hypotheses	lhpocnel2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lhpocnel2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lhpocnel2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lhpocnel2.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
Assertion	lhpocnel2	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$

Proof

Step	Hyp	Ref	Expression
1		lhpocnel2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lhpocnel2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		lhpocnel2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		lhpocnel2.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
5		eqid	$$⊢\mathrm{oc}\left(K\right)=\mathrm{oc}\left(K\right)$$
6	1 5 2 3	lhpocnel	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \left(\mathrm{oc}\left(K\right)\left(W\right)\in A\wedge \neg \mathrm{oc}\left(K\right)\left(W\right)\underset{\dot{}}{\le }W\right)$$
7	4	eleq1i	$$⊢P\in A\leftrightarrow \mathrm{oc}\left(K\right)\left(W\right)\in A$$
8	4	breq1i	$$⊢P\underset{\dot{}}{\le }W\leftrightarrow \mathrm{oc}\left(K\right)\left(W\right)\underset{\dot{}}{\le }W$$
9	8	notbii	$$⊢\neg P\underset{\dot{}}{\le }W\leftrightarrow \neg \mathrm{oc}\left(K\right)\left(W\right)\underset{\dot{}}{\le }W$$
10	7 9	anbi12i	$$⊢\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\mathrm{oc}\left(K\right)\left(W\right)\in A\wedge \neg \mathrm{oc}\left(K\right)\left(W\right)\underset{\dot{}}{\le }W\right)$$
11	6 10	sylibr	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$