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

Metamath Proof Explorer

Theorem pltval3

Description: Alternate expression for the "less than" relation. ( dfpss3 analog.) (Contributed by NM, 4-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		pleval2.b	$⊢ B = {Base}_{K}$
2		pleval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pleval2.s	$⊢ \underset{˙}{<} = <_{K}$
4	2 3	pltval	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
5	1 2	posref	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\leq} X$
6	5	3adant3	$⊢ (K \in Poset \land X \in B \land Y \in B) \to X \underset{˙}{\leq} X$
7		breq1	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow Y \underset{˙}{\leq} X)$
8	6 7	syl5ibcom	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X = Y \to Y \underset{˙}{\leq} X)$
9	8	adantr	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X = Y \to Y \underset{˙}{\leq} X)$
10	1 2	posasymb	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow X = Y)$
11	10	biimpd	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y)$
12	11	expdimp	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (Y \underset{˙}{\leq} X \to X = Y)$
13	9 12	impbid	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X = Y \leftrightarrow Y \underset{˙}{\leq} X)$
14	13	necon3abid	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X \neq Y \leftrightarrow \neg Y \underset{˙}{\leq} X)$
15	14	pm5.32da	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land X \neq Y) \leftrightarrow (X \underset{˙}{\leq} Y \land \neg Y \underset{˙}{\leq} X))$
16	4 15	bitrd	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land \neg Y \underset{˙}{\leq} X))$