xrletri3

Description: Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009)

		Ref	Expression
	Assertion	xrletri3	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$

Step	Hyp	Ref	Expression
1		xrlttri3	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \leftrightarrow (\neg A < B \land \neg B < A))$
2	1	biancomd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \leftrightarrow (\neg B < A \land \neg A < B))$
3		xrlenlt	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \leftrightarrow \neg B < A)$
4		xrlenlt	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B \leq A \leftrightarrow \neg A < B)$
5	4	ancoms	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B \leq A \leftrightarrow \neg A < B)$
6	3 5	anbi12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \leq B \land B \leq A) \leftrightarrow (\neg B < A \land \neg A < B))$
7	2 6	bitr4d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$

Metamath Proof Explorer