pltval

Description: Less-than relation. ( df-pss analog.) (Contributed by NM, 12-Oct-2011)

	Ref	Expression
Hypotheses	pltval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pltval.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	pltval	$⊢ (K \in A \land X \in B \land Y \in C) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$

Step	Hyp	Ref	Expression
1		pltval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		pltval.s	$⊢ \underset{˙}{<} = <_{K}$
3	1 2	pltfval	$⊢ K \in A \to \underset{˙}{<} = \underset{˙}{\leq} ∖ I$
4	3	breqd	$⊢ K \in A \to (X \underset{˙}{<} Y \leftrightarrow X (\underset{˙}{\leq} ∖ I) Y)$
5		brdif	$⊢ X (\underset{˙}{\leq} ∖ I) Y \leftrightarrow (X \underset{˙}{\leq} Y \land \neg X I Y)$
6		ideqg	$⊢ Y \in C \to (X I Y \leftrightarrow X = Y)$
7	6	necon3bbid	$⊢ Y \in C \to (\neg X I Y \leftrightarrow X \neq Y)$
8	7	adantl	$⊢ (X \in B \land Y \in C) \to (\neg X I Y \leftrightarrow X \neq Y)$
9	8	anbi2d	$⊢ (X \in B \land Y \in C) \to ((X \underset{˙}{\leq} Y \land \neg X I Y) \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
10	5 9	bitrid	$⊢ (X \in B \land Y \in C) \to (X (\underset{˙}{\leq} ∖ I) Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
11	4 10	sylan9bb	$⊢ (K \in A \land (X \in B \land Y \in C)) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
12	11	3impb	$⊢ (K \in A \land X \in B \land Y \in C) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$

Metamath Proof Explorer