tlt3

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

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

Step	Hyp	Ref	Expression
1		tlt3.b	$⊢ B = {Base}_{K}$
2		tlt3.l	$⊢ \underset{˙}{<} = <_{K}$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	1 3 2	tlt2	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \leq_{K} Y \lor Y \underset{˙}{<} X)$
5		tospos	$⊢ K \in Toset \to K \in Poset$
6	1 3 2	pleval2	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \leq_{K} Y \leftrightarrow (X \underset{˙}{<} Y \lor X = Y))$
7		orcom	$⊢ (X \underset{˙}{<} Y \lor X = Y) \leftrightarrow (X = Y \lor X \underset{˙}{<} Y)$
8	6 7	bitrdi	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \leq_{K} Y \leftrightarrow (X = Y \lor X \underset{˙}{<} Y))$
9	5 8	syl3an1	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \leq_{K} Y \leftrightarrow (X = Y \lor X \underset{˙}{<} Y))$
10	9	orbi1d	$⊢ (K \in Toset \land X \in B \land Y \in B) \to ((X \leq_{K} Y \lor Y \underset{˙}{<} X) \leftrightarrow ((X = Y \lor X \underset{˙}{<} Y) \lor Y \underset{˙}{<} X))$
11	4 10	mpbid	$⊢ (K \in Toset \land X \in B \land Y \in B) \to ((X = Y \lor X \underset{˙}{<} Y) \lor Y \underset{˙}{<} X)$
12		df-3or	$⊢ (X = Y \lor X \underset{˙}{<} Y \lor Y \underset{˙}{<} X) \leftrightarrow ((X = Y \lor X \underset{˙}{<} Y) \lor Y \underset{˙}{<} X)$
13	11 12	sylibr	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X = Y \lor X \underset{˙}{<} Y \lor Y \underset{˙}{<} X)$

Metamath Proof Explorer