pleval2i

Description: One direction of pleval2 . (Contributed 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	pleval2i	$⊢ (X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{<} Y \lor X = Y))$

Step	Hyp	Ref	Expression
1		pleval2.b	$⊢ B = {Base}_{K}$
2		pleval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pleval2.s	$⊢ \underset{˙}{<} = <_{K}$
4		elfvdm	$⊢ X \in {Base}_{K} \to K \in dom Base$
5	4 1	eleq2s	$⊢ X \in B \to K \in dom Base$
6	5	adantr	$⊢ (X \in B \land Y \in B) \to K \in dom Base$
7	2 3	pltval	$⊢ (K \in dom Base \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
8	7	3expb	$⊢ (K \in dom Base \land (X \in B \land Y \in B)) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
9	6 8	mpancom	$⊢ (X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
10	9	biimpar	$⊢ ((X \in B \land Y \in B) \land (X \underset{˙}{\leq} Y \land X \neq Y)) \to X \underset{˙}{<} Y$
11	10	expr	$⊢ ((X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X \neq Y \to X \underset{˙}{<} Y)$
12	11	necon1bd	$⊢ ((X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (\neg X \underset{˙}{<} Y \to X = Y)$
13	12	orrd	$⊢ ((X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{<} Y \lor X = Y)$
14	13	ex	$⊢ (X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{<} Y \lor X = Y))$

Metamath Proof Explorer