tlt2

Description: In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018)

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

Step	Hyp	Ref	Expression
1		tlt2.b	$⊢ B = {Base}_{K}$
2		tlt2.e	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		tlt2.l	$⊢ \underset{˙}{<} = <_{K}$
4		exmidd	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \lor \neg X \underset{˙}{\leq} Y)$
5	1 2 3	tltnle	$⊢ (K \in Toset \land Y \in B \land X \in B) \to (Y \underset{˙}{<} X \leftrightarrow \neg X \underset{˙}{\leq} Y)$
6	5	3com23	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (Y \underset{˙}{<} X \leftrightarrow \neg X \underset{˙}{\leq} Y)$
7	6	orbi2d	$⊢ (K \in Toset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \lor Y \underset{˙}{<} X) \leftrightarrow (X \underset{˙}{\leq} Y \lor \neg X \underset{˙}{\leq} Y))$
8	4 7	mpbird	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \lor Y \underset{˙}{<} X)$

Metamath Proof Explorer