posrasymb

Description: A poset ordering is asymmetric. (Contributed by Thierry Arnoux, 13-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		posrasymb.b	$⊢ B = {Base}_{K}$
2		posrasymb.l	$⊢ \underset{˙}{\leq} = \leq_{K} \cap (B \times B)$
3	2	breqi	$⊢ X \underset{˙}{\leq} Y \leftrightarrow X (\leq_{K} \cap (B \times B)) Y$
4		simp2	$⊢ (K \in Poset \land X \in B \land Y \in B) \to X \in B$
5		simp3	$⊢ (K \in Poset \land X \in B \land Y \in B) \to Y \in B$
6		brxp	$⊢ X (B \times B) Y \leftrightarrow (X \in B \land Y \in B)$
7	4 5 6	sylanbrc	$⊢ (K \in Poset \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 Poset \land X \in B \land Y \in B) \to (X (\leq_{K} \cap (B \times B)) Y \leftrightarrow X \leq_{K} Y)$
11	3 10	bitrid	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow X \leq_{K} Y)$
12	2	breqi	$⊢ Y \underset{˙}{\leq} X \leftrightarrow Y (\leq_{K} \cap (B \times B)) X$
13		brxp	$⊢ Y (B \times B) X \leftrightarrow (Y \in B \land X \in B)$
14	5 4 13	sylanbrc	$⊢ (K \in Poset \land X \in B \land Y \in B) \to Y (B \times B) X$
15		brin	$⊢ Y (\leq_{K} \cap (B \times B)) X \leftrightarrow (Y \leq_{K} X \land Y (B \times B) X)$
16	15	rbaib	$⊢ Y (B \times B) X \to (Y (\leq_{K} \cap (B \times B)) X \leftrightarrow Y \leq_{K} X)$
17	14 16	syl	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (Y (\leq_{K} \cap (B \times B)) X \leftrightarrow Y \leq_{K} X)$
18	12 17	bitrid	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (Y \underset{˙}{\leq} X \leftrightarrow Y \leq_{K} X)$
19	11 18	anbi12d	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow (X \leq_{K} Y \land Y \leq_{K} X))$
20		eqid	$⊢ \leq_{K} = \leq_{K}$
21	1 20	posasymb	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \leq_{K} Y \land Y \leq_{K} X) \leftrightarrow X = Y)$
22	19 21	bitrd	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem posrasymb

Proof