ncvr1

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

	Ref	Expression
Hypotheses	ncvr1.b	$⊢ B = {Base}_{K}$
	ncvr1.u	$⊢ \underset{˙}{1} = 1. (K)$
	ncvr1.c	$⊢ C = ⋖_{K}$
Assertion	ncvr1	$⊢ (K \in OP \land X \in B) \to \neg \underset{˙}{1} C X$

Proof

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

Metamath Proof Explorer

Theorem ncvr1

Proof