Theorem 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	$$⊢\le =<\cup \left({\mathrm{I}\upharpoonright }_{{ℝ}^{*}}\right)$$

Proof

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