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

Metamath Proof Explorer

Theorem latasym

Description: A lattice ordering is asymmetric. ( eqss analog.) (Contributed by NM, 8-Oct-2011)

	Ref	Expression
Hypotheses	latref.b	$⊢ B = {Base}_{K}$
	latref.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
Assertion	latasym	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y)$

Step	Hyp	Ref	Expression
1		latref.b	$⊢ B = {Base}_{K}$
2		latref.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3	1 2	latasymb	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow X = Y)$
4	3	biimpd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y)$