xrletri

Description: Trichotomy law for extended reals. (Contributed by NM, 7-Feb-2007)

		Ref	Expression
	Assertion	xrletri	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \lor B \leq A)$

Step	Hyp	Ref	Expression
1		xrltnle	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B < A \leftrightarrow \neg A \leq B)$
2	1	ancoms	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B < A \leftrightarrow \neg A \leq B)$
3		xrltle	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B < A \to B \leq A)$
4	3	ancoms	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B < A \to B \leq A)$
5	2 4	sylbird	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg A \leq B \to B \leq A)$
6	5	orrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \lor B \leq A)$

Metamath Proof Explorer