dfle2

Description: Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015)

		Ref	Expression
	Assertion	dfle2	$⊢ \leq = < \cup ({I ↾}_{ℝ^{*}})$

Step	Hyp	Ref	Expression
1		lerel	$⊢ Rel \leq$
2		ltrelxr	$⊢ < \subseteq ℝ^{} \times ℝ^{}$
3		idssxp	$⊢ {I ↾}_{ℝ^{}} \subseteq ℝ^{} \times ℝ^{*}$
4	2 3	unssi	$⊢ < \cup ({I ↾}_{ℝ^{}}) \subseteq ℝ^{} \times ℝ^{*}$
5		relxp	$⊢ Rel (ℝ^{} \times ℝ^{})$
6		relss	$⊢ < \cup ({I ↾}_{ℝ^{}}) \subseteq ℝ^{} \times ℝ^{} \to (Rel (ℝ^{} \times ℝ^{}) \to Rel (< \cup ({I ↾}_{ℝ^{}})))$
7	4 5 6	mp2	$⊢ Rel (< \cup ({I ↾}_{ℝ^{*}}))$
8		lerelxr	$⊢ \leq \subseteq ℝ^{} \times ℝ^{}$
9	8	brel	$⊢ x \leq y \to (x \in ℝ^{} \land y \in ℝ^{})$
10	4	brel	$⊢ x (< \cup ({I ↾}_{ℝ^{}})) y \to (x \in ℝ^{} \land y \in ℝ^{*})$
11		xrleloe	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \leftrightarrow (x < y \lor x = y))$
12		resieq	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x ({I ↾}_{ℝ^{*}}) y \leftrightarrow x = y)$
13	12	orbi2d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to ((x < y \lor x ({I ↾}_{ℝ^{*}}) y) \leftrightarrow (x < y \lor x = y))$
14	11 13	bitr4d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \leftrightarrow (x < y \lor x ({I ↾}_{ℝ^{*}}) y))$
15		brun	$⊢ x (< \cup ({I ↾}_{ℝ^{}})) y \leftrightarrow (x < y \lor x ({I ↾}_{ℝ^{}}) y)$
16	14 15	bitr4di	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \leftrightarrow x (< \cup ({I ↾}_{ℝ^{*}})) y)$
17	9 10 16	pm5.21nii	$⊢ x \leq y \leftrightarrow x (< \cup ({I ↾}_{ℝ^{*}})) y$
18	1 7 17	eqbrriv	$⊢ \leq = < \cup ({I ↾}_{ℝ^{*}})$

Metamath Proof Explorer