Theorem dflt2

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

	Ref	Expression
Assertion	dflt2	$$⊢<=\le \setminus \mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		ltrel	$$⊢\mathrm{Rel}<$$
2		difss	$$⊢\le \setminus \mathrm{I}\subseteq \le$$
3		lerel	$$⊢\mathrm{Rel}\le$$
4		relss	$$⊢\le \setminus \mathrm{I}\subseteq \le \to \left(\mathrm{Rel}\le \to \mathrm{Rel}\left(\le \setminus \mathrm{I}\right)\right)$$
5	2 3 4	mp2	$$⊢\mathrm{Rel}\left(\le \setminus \mathrm{I}\right)$$
6		ltrelxr	$$⊢<\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
7	6	brel	$$⊢x<y\to \left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)$$
8		lerelxr	$$⊢\le \subseteq {ℝ}^{*}\times {ℝ}^{*}$$
9	2 8	sstri	$$⊢\le \setminus \mathrm{I}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
10	9	brel	$$⊢x\left(\le \setminus \mathrm{I}\right)y\to \left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)$$
11		xrltlen	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x<y\leftrightarrow \left(x\le y\wedge y\ne x\right)\right)$$
12		equcom	$$⊢y=x\leftrightarrow x=y$$
13		vex	$$⊢y\in \mathrm{V}$$
14	13	ideq	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
15	12 14	bitr4i	$$⊢y=x\leftrightarrow x\mathrm{I}y$$
16	15	necon3abii	$$⊢y\ne x\leftrightarrow \neg x\mathrm{I}y$$
17	16	anbi2i	$$⊢\left(x\le y\wedge y\ne x\right)\leftrightarrow \left(x\le y\wedge \neg x\mathrm{I}y\right)$$
18	11 17	bitrdi	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x<y\leftrightarrow \left(x\le y\wedge \neg x\mathrm{I}y\right)\right)$$
19		brdif	$$⊢x\left(\le \setminus \mathrm{I}\right)y\leftrightarrow \left(x\le y\wedge \neg x\mathrm{I}y\right)$$
20	18 19	bitr4di	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x<y\leftrightarrow x\left(\le \setminus \mathrm{I}\right)y\right)$$
21	7 10 20	pm5.21nii	$$⊢x<y\leftrightarrow x\left(\le \setminus \mathrm{I}\right)y$$
22	1 5 21	eqbrriv	$$⊢<=\le \setminus \mathrm{I}$$