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

Metamath Proof Explorer

Theorem latref

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

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

Step	Hyp	Ref	Expression
1		latref.b	$⊢ B = {Base}_{K}$
2		latref.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		latpos	$⊢ K \in Lat \to K \in Poset$
4	1 2	posref	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\leq} X$
5	3 4	sylan	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\leq} X$