Theorem icorempo

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

	Ref	Expression
Hypothesis	icorempo.1	⊢ 𝐹 = ( [,) ↾ ( ℝ × ℝ ) )
Assertion	icorempo	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )

Proof

Step	Hyp	Ref	Expression
1		icorempo.1	⊢ 𝐹 = ( [,) ↾ ( ℝ × ℝ ) )
2		df-ico	⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
3	2	reseq1i	⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) )
4		ressxr	⊢ ℝ ⊆ ℝ*
5		resmpo	⊢ ( ( ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ* ) → ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) )
6	4 4 5	mp2an	⊢ ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
7	3 6	eqtri	⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
8		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ )
9		nfrab1	⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) }
10		nfrab1	⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) }
11		rabid	⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ↔ ( 𝑧 ∈ ℝ* ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ) )
12		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
13		nltmnf	⊢ ( 𝑥 ∈ ℝ* → ¬ 𝑥 < -∞ )
14	12 13	syl	⊢ ( 𝑥 ∈ ℝ → ¬ 𝑥 < -∞ )
15		renemnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 ≠ -∞ )
16	15	neneqd	⊢ ( 𝑥 ∈ ℝ → ¬ 𝑥 = -∞ )
17	14 16	jca	⊢ ( 𝑥 ∈ ℝ → ( ¬ 𝑥 < -∞ ∧ ¬ 𝑥 = -∞ ) )
18		pm4.56	⊢ ( ( ¬ 𝑥 < -∞ ∧ ¬ 𝑥 = -∞ ) ↔ ¬ ( 𝑥 < -∞ ∨ 𝑥 = -∞ ) )
19	17 18	sylib	⊢ ( 𝑥 ∈ ℝ → ¬ ( 𝑥 < -∞ ∨ 𝑥 = -∞ ) )
20		mnfxr	⊢ -∞ ∈ ℝ*
21		xrleloe	⊢ ( ( 𝑥 ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( 𝑥 ≤ -∞ ↔ ( 𝑥 < -∞ ∨ 𝑥 = -∞ ) ) )
22	12 20 21	sylancl	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ≤ -∞ ↔ ( 𝑥 < -∞ ∨ 𝑥 = -∞ ) ) )
23	19 22	mtbird	⊢ ( 𝑥 ∈ ℝ → ¬ 𝑥 ≤ -∞ )
24		breq2	⊢ ( 𝑧 = -∞ → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ≤ -∞ ) )
25	24	notbid	⊢ ( 𝑧 = -∞ → ( ¬ 𝑥 ≤ 𝑧 ↔ ¬ 𝑥 ≤ -∞ ) )
26	23 25	syl5ibrcom	⊢ ( 𝑥 ∈ ℝ → ( 𝑧 = -∞ → ¬ 𝑥 ≤ 𝑧 ) )
27	26	con2d	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ≤ 𝑧 → ¬ 𝑧 = -∞ ) )
28		rexr	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
29		pnfnlt	⊢ ( 𝑦 ∈ ℝ* → ¬ +∞ < 𝑦 )
30		breq1	⊢ ( 𝑧 = +∞ → ( 𝑧 < 𝑦 ↔ +∞ < 𝑦 ) )
31	30	notbid	⊢ ( 𝑧 = +∞ → ( ¬ 𝑧 < 𝑦 ↔ ¬ +∞ < 𝑦 ) )
32	29 31	syl5ibrcom	⊢ ( 𝑦 ∈ ℝ* → ( 𝑧 = +∞ → ¬ 𝑧 < 𝑦 ) )
33	32	con2d	⊢ ( 𝑦 ∈ ℝ* → ( 𝑧 < 𝑦 → ¬ 𝑧 = +∞ ) )
34	28 33	syl	⊢ ( 𝑦 ∈ ℝ → ( 𝑧 < 𝑦 → ¬ 𝑧 = +∞ ) )
35	27 34	im2anan9	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) → ( ¬ 𝑧 = -∞ ∧ ¬ 𝑧 = +∞ ) ) )
36	35	anim2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ ℝ* ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ) → ( 𝑧 ∈ ℝ* ∧ ( ¬ 𝑧 = -∞ ∧ ¬ 𝑧 = +∞ ) ) ) )
37		renepnf	⊢ ( 𝑧 ∈ ℝ → 𝑧 ≠ +∞ )
38	37	neneqd	⊢ ( 𝑧 ∈ ℝ → ¬ 𝑧 = +∞ )
39	38	pm4.71i	⊢ ( 𝑧 ∈ ℝ ↔ ( 𝑧 ∈ ℝ ∧ ¬ 𝑧 = +∞ ) )
40		xrnemnf	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑧 ≠ -∞ ) ↔ ( 𝑧 ∈ ℝ ∨ 𝑧 = +∞ ) )
41	40	anbi1i	⊢ ( ( ( 𝑧 ∈ ℝ* ∧ 𝑧 ≠ -∞ ) ∧ ¬ 𝑧 = +∞ ) ↔ ( ( 𝑧 ∈ ℝ ∨ 𝑧 = +∞ ) ∧ ¬ 𝑧 = +∞ ) )
42		df-ne	⊢ ( 𝑧 ≠ -∞ ↔ ¬ 𝑧 = -∞ )
43	42	anbi2i	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑧 ≠ -∞ ) ↔ ( 𝑧 ∈ ℝ* ∧ ¬ 𝑧 = -∞ ) )
44	43	anbi1i	⊢ ( ( ( 𝑧 ∈ ℝ* ∧ 𝑧 ≠ -∞ ) ∧ ¬ 𝑧 = +∞ ) ↔ ( ( 𝑧 ∈ ℝ* ∧ ¬ 𝑧 = -∞ ) ∧ ¬ 𝑧 = +∞ ) )
45		pm5.61	⊢ ( ( ( 𝑧 ∈ ℝ ∨ 𝑧 = +∞ ) ∧ ¬ 𝑧 = +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ ¬ 𝑧 = +∞ ) )
46	41 44 45	3bitr3i	⊢ ( ( ( 𝑧 ∈ ℝ* ∧ ¬ 𝑧 = -∞ ) ∧ ¬ 𝑧 = +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ ¬ 𝑧 = +∞ ) )
47		anass	⊢ ( ( ( 𝑧 ∈ ℝ* ∧ ¬ 𝑧 = -∞ ) ∧ ¬ 𝑧 = +∞ ) ↔ ( 𝑧 ∈ ℝ* ∧ ( ¬ 𝑧 = -∞ ∧ ¬ 𝑧 = +∞ ) ) )
48	39 46 47	3bitr2ri	⊢ ( ( 𝑧 ∈ ℝ* ∧ ( ¬ 𝑧 = -∞ ∧ ¬ 𝑧 = +∞ ) ) ↔ 𝑧 ∈ ℝ )
49	36 48	syl6ib	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ ℝ* ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ) → 𝑧 ∈ ℝ ) )
50	11 49	syl5bi	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → 𝑧 ∈ ℝ ) )
51	11	simprbi	⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) )
52	51	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ) )
53	50 52	jcad	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ) ) )
54		rabid	⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ) )
55	53 54	syl6ibr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) )
56		rabss2	⊢ ( ℝ ⊆ ℝ* → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
57	4 56	ax-mp	⊢ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) }
58	57	sseli	⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
59	55 58	impbid1	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ↔ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) )
60	8 9 10 59	eqrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
61	60	mpoeq3ia	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
62	1 7 61	3eqtri	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )