Theorem hlrelat1

Description: An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of MaedaMaeda p. 30. ( chpssati , with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011)

	Ref	Expression
Hypotheses	hlrelat1.b	$$⊢B={\mathrm{Base}}_K$$
	hlrelat1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlrelat1.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	hlrelat1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlrelat1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlrelat1.b	$$⊢B={\mathrm{Base}}_K$$
2		hlrelat1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		hlrelat1.s	$$⊢\underset{\dot{}}{<}={<}_K$$
4		hlrelat1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		hlomcmat	$$⊢K\in \mathrm{HL}\to \left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)$$
6	1 2 3 4	atlrelat1	$$⊢\left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)\right)$$
7	5 6	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)\right)$$