This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latnlemlt

Description: Negation of "less than or equal to" expressed in terms of meet and less-than. ( nssinpss analog.) (Contributed by NM, 5-Feb-2012)

		Ref	Expression
	Hypotheses	latnlemlt.b	$⊢ B = {Base}_{K}$
		latnlemlt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		latnlemlt.s	$⊢ \underset{˙}{<} = <_{K}$
		latnlemlt.m	$⊢ \underset{˙}{\land} = meet (K)$
	Assertion	latnlemlt	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (\neg X \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{<} X)$

Proof

Step	Hyp	Ref	Expression
1		latnlemlt.b	$⊢ B = {Base}_{K}$
2		latnlemlt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latnlemlt.s	$⊢ \underset{˙}{<} = <_{K}$
4		latnlemlt.m	$⊢ \underset{˙}{\land} = meet (K)$
5	1 2 4	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
6	5	biantrurd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y \neq X \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land X \underset{˙}{\land} Y \neq X))$
7	1 2 4	latleeqm1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\land} Y = X)$
8	7	necon3bbid	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (\neg X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\land} Y \neq X)$
9		simp1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to K \in Lat$
10	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
11		simp2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \in B$
12	2 3	pltval	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land X \in B) \to ((X \underset{˙}{\land} Y) \underset{˙}{<} X \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land X \underset{˙}{\land} Y \neq X))$
13	9 10 11 12	syl3anc	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) \underset{˙}{<} X \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\leq} X \land X \underset{˙}{\land} Y \neq X))$
14	6 8 13	3bitr4d	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (\neg X \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{<} X)$