trleile

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

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

Proof

Step	Hyp	Ref	Expression
1		trleile.b	$⊢ B = {Base}_{K}$
2		trleile.l	$⊢ \underset{˙}{\leq} = \leq_{K} \cap (B \times B)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	1 3	tleile	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \leq_{K} Y \lor Y \leq_{K} X)$
5		3simpc	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \in B \land Y \in B)$
6		brxp	$⊢ X (B \times B) Y \leftrightarrow (X \in B \land Y \in B)$
7	5 6	sylibr	$⊢ (K \in Toset \land X \in B \land Y \in B) \to X (B \times B) Y$
8		brin	$⊢ X (\leq_{K} \cap (B \times B)) Y \leftrightarrow (X \leq_{K} Y \land X (B \times B) Y)$
9	8	rbaib	$⊢ X (B \times B) Y \to (X (\leq_{K} \cap (B \times B)) Y \leftrightarrow X \leq_{K} Y)$
10	7 9	syl	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X (\leq_{K} \cap (B \times B)) Y \leftrightarrow X \leq_{K} Y)$
11	5	ancomd	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (Y \in B \land X \in B)$
12		brxp	$⊢ Y (B \times B) X \leftrightarrow (Y \in B \land X \in B)$
13	11 12	sylibr	$⊢ (K \in Toset \land X \in B \land Y \in B) \to Y (B \times B) X$
14		brin	$⊢ Y (\leq_{K} \cap (B \times B)) X \leftrightarrow (Y \leq_{K} X \land Y (B \times B) X)$
15	14	rbaib	$⊢ Y (B \times B) X \to (Y (\leq_{K} \cap (B \times B)) X \leftrightarrow Y \leq_{K} X)$
16	13 15	syl	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (Y (\leq_{K} \cap (B \times B)) X \leftrightarrow Y \leq_{K} X)$
17	10 16	orbi12d	$⊢ (K \in Toset \land X \in B \land Y \in B) \to ((X (\leq_{K} \cap (B \times B)) Y \lor Y (\leq_{K} \cap (B \times B)) X) \leftrightarrow (X \leq_{K} Y \lor Y \leq_{K} X))$
18	4 17	mpbird	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X (\leq_{K} \cap (B \times B)) Y \lor Y (\leq_{K} \cap (B \times B)) X)$
19	2	breqi	$⊢ X \underset{˙}{\leq} Y \leftrightarrow X (\leq_{K} \cap (B \times B)) Y$
20	2	breqi	$⊢ Y \underset{˙}{\leq} X \leftrightarrow Y (\leq_{K} \cap (B \times B)) X$
21	19 20	orbi12i	$⊢ (X \underset{˙}{\leq} Y \lor Y \underset{˙}{\leq} X) \leftrightarrow (X (\leq_{K} \cap (B \times B)) Y \lor Y (\leq_{K} \cap (B \times B)) X)$
22	18 21	sylibr	$⊢ (K \in Toset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \lor Y \underset{˙}{\leq} X)$

Metamath Proof Explorer

Theorem trleile

Proof