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

Metamath Proof Explorer

Theorem pleval2

Description: "Less than or equal to" in terms of "less than". ( sspss analog.) (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 8-Feb-2015)

		Ref	Expression
	Hypotheses	pleval2.b	$⊢ B = {Base}_{K}$
		pleval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		pleval2.s	$⊢ \underset{˙}{<} = <_{K}$
	Assertion	pleval2	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{<} Y \lor X = Y))$

Proof

Step	Hyp	Ref	Expression
1		pleval2.b	$⊢ B = {Base}_{K}$
2		pleval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pleval2.s	$⊢ \underset{˙}{<} = <_{K}$
4	1 2 3	pleval2i	$⊢ (X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{<} Y \lor X = Y))$
5	4	3adant1	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{<} Y \lor X = Y))$
6	2 3	pltle	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \underset{˙}{\leq} Y)$
7	1 2	posref	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\leq} X$
8	7	3adant3	$⊢ (K \in Poset \land X \in B \land Y \in B) \to X \underset{˙}{\leq} X$
9		breq2	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\leq} Y)$
10	8 9	syl5ibcom	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X = Y \to X \underset{˙}{\leq} Y)$
11	6 10	jaod	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{<} Y \lor X = Y) \to X \underset{˙}{\leq} Y)$
12	5 11	impbid	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{<} Y \lor X = Y))$