Theorem iscvlat2N

Description: The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	iscvlat2.b	$$⊢B={\mathrm{Base}}_K$$
	iscvlat2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	iscvlat2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	iscvlat2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	iscvlat2.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	iscvlat2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	iscvlat2N	$$⊢K\in \mathrm{CvLat}\leftrightarrow \left(K\in \mathrm{AtLat}\wedge \forall p\in A\forall q\in A\forall x\in B\left(\left(p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscvlat2.b	$$⊢B={\mathrm{Base}}_K$$
2		iscvlat2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		iscvlat2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		iscvlat2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		iscvlat2.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
6		iscvlat2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
7	1 2 3 6	iscvlat	$$⊢K\in \mathrm{CvLat}\leftrightarrow \left(K\in \mathrm{AtLat}\wedge \forall p\in A\forall q\in A\forall x\in B\left(\left(\neg p\underset{\dot{}}{\le }x\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)$$
8		simpll	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge \left(p\in A\wedge q\in A\right)\right)\wedge x\in B\right)\to K\in \mathrm{AtLat}$$
9		simplrl	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge \left(p\in A\wedge q\in A\right)\right)\wedge x\in B\right)\to p\in A$$
10		simpr	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge \left(p\in A\wedge q\in A\right)\right)\wedge x\in B\right)\to x\in B$$
11	1 2 4 5 6	atnle	$$⊢\left(K\in \mathrm{AtLat}\wedge p\in A\wedge x\in B\right)\to \left(\neg p\underset{\dot{}}{\le }x\leftrightarrow p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\right)$$
12	8 9 10 11	syl3anc	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge \left(p\in A\wedge q\in A\right)\right)\wedge x\in B\right)\to \left(\neg p\underset{\dot{}}{\le }x\leftrightarrow p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\right)$$
13	12	anbi1d	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge \left(p\in A\wedge q\in A\right)\right)\wedge x\in B\right)\to \left(\left(\neg p\underset{\dot{}}{\le }x\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\right)$$
14	13	imbi1d	$$⊢\left(\left(K\in \mathrm{AtLat}\wedge \left(p\in A\wedge q\in A\right)\right)\wedge x\in B\right)\to \left(\left(\left(\neg p\underset{\dot{}}{\le }x\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)$$
15	14	ralbidva	$$⊢\left(K\in \mathrm{AtLat}\wedge \left(p\in A\wedge q\in A\right)\right)\to \left(\forall x\in B\left(\left(\neg p\underset{\dot{}}{\le }x\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\leftrightarrow \forall x\in B\left(\left(p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)$$
16	15	2ralbidva	$$⊢K\in \mathrm{AtLat}\to \left(\forall p\in A\forall q\in A\forall x\in B\left(\left(\neg p\underset{\dot{}}{\le }x\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\leftrightarrow \forall p\in A\forall q\in A\forall x\in B\left(\left(p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)$$
17	16	pm5.32i	$$⊢\left(K\in \mathrm{AtLat}\wedge \forall p\in A\forall q\in A\forall x\in B\left(\left(\neg p\underset{\dot{}}{\le }x\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)\leftrightarrow \left(K\in \mathrm{AtLat}\wedge \forall p\in A\forall q\in A\forall x\in B\left(\left(p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)$$
18	7 17	bitri	$$⊢K\in \mathrm{CvLat}\leftrightarrow \left(K\in \mathrm{AtLat}\wedge \forall p\in A\forall q\in A\forall x\in B\left(\left(p\underset{\dot{}}{\wedge }x=\underset{\dot{}}{0}\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\to q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)\right)$$