Theorem ncvr1

Description: No element covers the lattice unity. (Contributed by NM, 8-Jul-2013)

	Ref	Expression
Hypotheses	ncvr1.b	$$⊢B={\mathrm{Base}}_K$$
	ncvr1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	ncvr1.c	$$⊢C={⋖}_K$$
Assertion	ncvr1	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \neg \underset{\dot{}}{1}CX$$

Proof

Step	Hyp	Ref	Expression
1		ncvr1.b	$$⊢B={\mathrm{Base}}_K$$
2		ncvr1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
3		ncvr1.c	$$⊢C={⋖}_K$$
4		eqid	$$⊢{\le }_K={\le }_K$$
5	1 4 2	ople1	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X{\le }_K\underset{\dot{}}{1}$$
6		opposet	$$⊢K\in \mathrm{OP}\to K\in \mathrm{Poset}$$
7	6	ad2antrr	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}{<}_{K}X\right)\to K\in \mathrm{Poset}$$
8	1 2	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in B$$
9	8	ad2antrr	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}{<}_{K}X\right)\to \underset{\dot{}}{1}\in B$$
10		simplr	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}{<}_{K}X\right)\to X\in B$$
11		simpr	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}{<}_{K}X\right)\to \underset{\dot{}}{1}{<}_{K}X$$
12		eqid	$$⊢{<}_K={<}_K$$
13	1 4 12	pltnle	$$⊢\left(\left(K\in \mathrm{Poset}\wedge \underset{\dot{}}{1}\in B\wedge X\in B\right)\wedge \underset{\dot{}}{1}{<}_{K}X\right)\to \neg X{\le }_K\underset{\dot{}}{1}$$
14	7 9 10 11 13	syl31anc	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}{<}_{K}X\right)\to \neg X{\le }_K\underset{\dot{}}{1}$$
15	14	ex	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \left(\underset{\dot{}}{1}{<}_{K}X\to \neg X{\le }_K\underset{\dot{}}{1}\right)$$
16	5 15	mt2d	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \neg \underset{\dot{}}{1}{<}_{K}X$$
17		simpll	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}CX\right)\to K\in \mathrm{OP}$$
18	8	ad2antrr	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}CX\right)\to \underset{\dot{}}{1}\in B$$
19		simplr	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}CX\right)\to X\in B$$
20		simpr	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}CX\right)\to \underset{\dot{}}{1}CX$$
21	1 12 3	cvrlt	$$⊢\left(\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{1}\in B\wedge X\in B\right)\wedge \underset{\dot{}}{1}CX\right)\to \underset{\dot{}}{1}{<}_{K}X$$
22	17 18 19 20 21	syl31anc	$$⊢\left(\left(K\in \mathrm{OP}\wedge X\in B\right)\wedge \underset{\dot{}}{1}CX\right)\to \underset{\dot{}}{1}{<}_{K}X$$
23	16 22	mtand	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \neg \underset{\dot{}}{1}CX$$