icorempo

Description: Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020)

		Ref	Expression
	Hypothesis	icorempo.1	$⊢ F = {[.) ↾}_{ℝ^{2}}$
	Assertion	icorempo	$⊢ F = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\})$

Proof

Step	Hyp	Ref	Expression
1		icorempo.1	$⊢ F = {[.) ↾}_{ℝ^{2}}$
2		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
3	2	reseq1i	$⊢ {[.) ↾}_{ℝ^{2}} = {(x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\}) ↾}_{ℝ^{2}}$
4		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
5		resmpo	$⊢ (ℝ \subseteq ℝ^{} \land ℝ \subseteq ℝ^{}) \to {(x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\}) ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\})$
6	4 4 5	mp2an	$⊢ {(x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\}) ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\})$
7	3 6	eqtri	$⊢ {[.) ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
8		nfv	$⊢ Ⅎ z (x \in ℝ \land y \in ℝ)$
9		nfrab1	$⊢ \underline{Ⅎ} z \{z \in ℝ^{*} \| (x \leq z \land z < y)\}$
10		nfrab1	$⊢ \underline{Ⅎ} z \{z \in ℝ \| (x \leq z \land z < y)\}$
11		rabid	$⊢ z \in \{z \in ℝ^{} \| (x \leq z \land z < y)\} \leftrightarrow (z \in ℝ^{} \land (x \leq z \land z < y))$
12		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
13		nltmnf	$⊢ x \in ℝ^{*} \to \neg x < −∞$
14	12 13	syl	$⊢ x \in ℝ \to \neg x < −∞$
15		renemnf	$⊢ x \in ℝ \to x \neq −∞$
16	15	neneqd	$⊢ x \in ℝ \to \neg x = −∞$
17	14 16	jca	$⊢ x \in ℝ \to (\neg x < −∞ \land \neg x = −∞)$
18		pm4.56	$⊢ (\neg x < −∞ \land \neg x = −∞) \leftrightarrow \neg (x < −∞ \lor x = −∞)$
19	17 18	sylib	$⊢ x \in ℝ \to \neg (x < −∞ \lor x = −∞)$
20		mnfxr	$⊢ −∞ \in ℝ^{*}$
21		xrleloe	$⊢ (x \in ℝ^{} \land −∞ \in ℝ^{}) \to (x \leq −∞ \leftrightarrow (x < −∞ \lor x = −∞))$
22	12 20 21	sylancl	$⊢ x \in ℝ \to (x \leq −∞ \leftrightarrow (x < −∞ \lor x = −∞))$
23	19 22	mtbird	$⊢ x \in ℝ \to \neg x \leq −∞$
24		breq2	$⊢ z = −∞ \to (x \leq z \leftrightarrow x \leq −∞)$
25	24	notbid	$⊢ z = −∞ \to (\neg x \leq z \leftrightarrow \neg x \leq −∞)$
26	23 25	syl5ibrcom	$⊢ x \in ℝ \to (z = −∞ \to \neg x \leq z)$
27	26	con2d	$⊢ x \in ℝ \to (x \leq z \to \neg z = −∞)$
28		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
29		pnfnlt	$⊢ y \in ℝ^{*} \to \neg +∞ < y$
30		breq1	$⊢ z = +∞ \to (z < y \leftrightarrow +∞ < y)$
31	30	notbid	$⊢ z = +∞ \to (\neg z < y \leftrightarrow \neg +∞ < y)$
32	29 31	syl5ibrcom	$⊢ y \in ℝ^{*} \to (z = +∞ \to \neg z < y)$
33	32	con2d	$⊢ y \in ℝ^{*} \to (z < y \to \neg z = +∞)$
34	28 33	syl	$⊢ y \in ℝ \to (z < y \to \neg z = +∞)$
35	27 34	im2anan9	$⊢ (x \in ℝ \land y \in ℝ) \to ((x \leq z \land z < y) \to (\neg z = −∞ \land \neg z = +∞))$
36	35	anim2d	$⊢ (x \in ℝ \land y \in ℝ) \to ((z \in ℝ^{} \land (x \leq z \land z < y)) \to (z \in ℝ^{} \land (\neg z = −∞ \land \neg z = +∞)))$
37		renepnf	$⊢ z \in ℝ \to z \neq +∞$
38	37	neneqd	$⊢ z \in ℝ \to \neg z = +∞$
39	38	pm4.71i	$⊢ z \in ℝ \leftrightarrow (z \in ℝ \land \neg z = +∞)$
40		xrnemnf	$⊢ (z \in ℝ^{*} \land z \neq −∞) \leftrightarrow (z \in ℝ \lor z = +∞)$
41	40	anbi1i	$⊢ ((z \in ℝ^{*} \land z \neq −∞) \land \neg z = +∞) \leftrightarrow ((z \in ℝ \lor z = +∞) \land \neg z = +∞)$
42		df-ne	$⊢ z \neq −∞ \leftrightarrow \neg z = −∞$
43	42	anbi2i	$⊢ (z \in ℝ^{} \land z \neq −∞) \leftrightarrow (z \in ℝ^{} \land \neg z = −∞)$
44	43	anbi1i	$⊢ ((z \in ℝ^{} \land z \neq −∞) \land \neg z = +∞) \leftrightarrow ((z \in ℝ^{} \land \neg z = −∞) \land \neg z = +∞)$
45		pm5.61	$⊢ ((z \in ℝ \lor z = +∞) \land \neg z = +∞) \leftrightarrow (z \in ℝ \land \neg z = +∞)$
46	41 44 45	3bitr3i	$⊢ ((z \in ℝ^{*} \land \neg z = −∞) \land \neg z = +∞) \leftrightarrow (z \in ℝ \land \neg z = +∞)$
47		anass	$⊢ ((z \in ℝ^{} \land \neg z = −∞) \land \neg z = +∞) \leftrightarrow (z \in ℝ^{} \land (\neg z = −∞ \land \neg z = +∞))$
48	39 46 47	3bitr2ri	$⊢ (z \in ℝ^{*} \land (\neg z = −∞ \land \neg z = +∞)) \leftrightarrow z \in ℝ$
49	36 48	imbitrdi	$⊢ (x \in ℝ \land y \in ℝ) \to ((z \in ℝ^{*} \land (x \leq z \land z < y)) \to z \in ℝ)$
50	11 49	biimtrid	$⊢ (x \in ℝ \land y \in ℝ) \to (z \in \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to z \in ℝ)$
51	11	simprbi	$⊢ z \in \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to (x \leq z \land z < y)$
52	51	a1i	$⊢ (x \in ℝ \land y \in ℝ) \to (z \in \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to (x \leq z \land z < y))$
53	50 52	jcad	$⊢ (x \in ℝ \land y \in ℝ) \to (z \in \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to (z \in ℝ \land (x \leq z \land z < y)))$
54		rabid	$⊢ z \in \{z \in ℝ \| (x \leq z \land z < y)\} \leftrightarrow (z \in ℝ \land (x \leq z \land z < y))$
55	53 54	imbitrrdi	$⊢ (x \in ℝ \land y \in ℝ) \to (z \in \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to z \in \{z \in ℝ \| (x \leq z \land z < y)\})$
56		rabss2	$⊢ ℝ \subseteq ℝ^{} \to \{z \in ℝ \| (x \leq z \land z < y)\} \subseteq \{z \in ℝ^{} \| (x \leq z \land z < y)\}$
57	4 56	ax-mp	$⊢ \{z \in ℝ \| (x \leq z \land z < y)\} \subseteq \{z \in ℝ^{*} \| (x \leq z \land z < y)\}$
58	57	sseli	$⊢ z \in \{z \in ℝ \| (x \leq z \land z < y)\} \to z \in \{z \in ℝ^{*} \| (x \leq z \land z < y)\}$
59	55 58	impbid1	$⊢ (x \in ℝ \land y \in ℝ) \to (z \in \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \leftrightarrow z \in \{z \in ℝ \| (x \leq z \land z < y)\})$
60	8 9 10 59	eqrd	$⊢ (x \in ℝ \land y \in ℝ) \to \{z \in ℝ^{*} \| (x \leq z \land z < y)\} = \{z \in ℝ \| (x \leq z \land z < y)\}$
61	60	mpoeq3ia	$⊢ (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\}) = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\})$
62	1 7 61	3eqtri	$⊢ F = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\})$

Metamath Proof Explorer

Theorem icorempo

Proof