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

Metamath Proof Explorer

Theorem posref

Description: A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011) (Proof shortened by OpenAI, 25-Mar-2020)

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

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