Theorem hlrelat5N

Description: An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of Kalmbach p. 149. (Contributed by NM, 21-Oct-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hlrelat5.b	$$⊢B={\mathrm{Base}}_K$$
2		hlrelat5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		hlrelat5.s	$$⊢\underset{\dot{}}{<}={<}_K$$
4		hlrelat5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5		hlrelat5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6	1 2 3 5	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)$$
7	6	imp	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to \exists p\in A\left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)$$
8		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
9		id	$$⊢X\in B\to X\in B$$
10	1 5	atbase	$$⊢p\in A\to p\in B$$
11		ovexd	$$⊢p\in B\to X\underset{\dot{}}{\vee }p\in \mathrm{V}$$
12	2 3	pltval	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge X\underset{\dot{}}{\vee }p\in \mathrm{V}\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\leftrightarrow \left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }p\right)\wedge X\ne X\underset{\dot{}}{\vee }p\right)\right)$$
13	11 12	syl3an3	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\leftrightarrow \left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }p\right)\wedge X\ne X\underset{\dot{}}{\vee }p\right)\right)$$
14	1 2 4	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }p\right)$$
15	14	biantrurd	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(X\ne X\underset{\dot{}}{\vee }p\leftrightarrow \left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }p\right)\wedge X\ne X\underset{\dot{}}{\vee }p\right)\right)$$
16	13 15	bitr4d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\leftrightarrow X\ne X\underset{\dot{}}{\vee }p\right)$$
17	1 2 4	latleeqj1	$$⊢\left(K\in \mathrm{Lat}\wedge p\in B\wedge X\in B\right)\to \left(p\underset{\dot{}}{\le }X\leftrightarrow p\underset{\dot{}}{\vee }X=X\right)$$
18	17	3com23	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(p\underset{\dot{}}{\le }X\leftrightarrow p\underset{\dot{}}{\vee }X=X\right)$$
19	1 4	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to X\underset{\dot{}}{\vee }p=p\underset{\dot{}}{\vee }X$$
20	19	eqeq1d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(X\underset{\dot{}}{\vee }p=X\leftrightarrow p\underset{\dot{}}{\vee }X=X\right)$$
21	18 20	bitr4d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(p\underset{\dot{}}{\le }X\leftrightarrow X\underset{\dot{}}{\vee }p=X\right)$$
22	21	notbid	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(\neg p\underset{\dot{}}{\le }X\leftrightarrow \neg X\underset{\dot{}}{\vee }p=X\right)$$
23		nesym	$$⊢X\ne X\underset{\dot{}}{\vee }p\leftrightarrow \neg X\underset{\dot{}}{\vee }p=X$$
24	22 23	syl6bbr	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(\neg p\underset{\dot{}}{\le }X\leftrightarrow X\ne X\underset{\dot{}}{\vee }p\right)$$
25	16 24	bitr4d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge p\in B\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\leftrightarrow \neg p\underset{\dot{}}{\le }X\right)$$
26	8 9 10 25	syl3an	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge p\in A\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\leftrightarrow \neg p\underset{\dot{}}{\le }X\right)$$
27	26	3expa	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge p\in A\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\leftrightarrow \neg p\underset{\dot{}}{\le }X\right)$$
28	27	anbi1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge p\in A\right)\to \left(\left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\wedge p\underset{\dot{}}{\le }Y\right)\leftrightarrow \left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)\right)$$
29	28	rexbidva	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\wedge p\underset{\dot{}}{\le }Y\right)\leftrightarrow \exists p\in A\left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)\right)$$
30	29	3adant3	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(\exists p\in A\left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\wedge p\underset{\dot{}}{\le }Y\right)\leftrightarrow \exists p\in A\left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)\right)$$
31	30	adantr	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to \left(\exists p\in A\left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\wedge p\underset{\dot{}}{\le }Y\right)\leftrightarrow \exists p\in A\left(\neg p\underset{\dot{}}{\le }X\wedge p\underset{\dot{}}{\le }Y\right)\right)$$
32	7 31	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to \exists p\in A\left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }p\right)\wedge p\underset{\dot{}}{\le }Y\right)$$