This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem posasymb

Description: A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011)

		Ref	Expression
	Hypotheses	posi.b	$⊢ B = {Base}_{K}$
		posi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	Assertion	posasymb	$⊢ (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		posi.b	$⊢ B = {Base}_{K}$
2		posi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		simp1	$⊢ (K \in Poset \land X \in B \land Y \in B) \to K \in Poset$
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	1 2	posi	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Y \in B)) \to (X \underset{˙}{\leq} X \land ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y) \land ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y))$
7	3 4 5 5 6	syl13anc	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} X \land ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y) \land ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y))$
8	7	simp2d	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y)$
9	1 2	posref	$⊢ (K \in Poset \land X \in B) \to X \underset{˙}{\leq} X$
10		breq2	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\leq} Y)$
11	9 10	syl5ibcom	$⊢ (K \in Poset \land X \in B) \to (X = Y \to X \underset{˙}{\leq} Y)$
12		breq1	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow Y \underset{˙}{\leq} X)$
13	9 12	syl5ibcom	$⊢ (K \in Poset \land X \in B) \to (X = Y \to Y \underset{˙}{\leq} X)$
14	11 13	jcad	$⊢ (K \in Poset \land X \in B) \to (X = Y \to (X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X))$
15	14	3adant3	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X = Y \to (X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X))$
16	8 15	impbid	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow X = Y)$