Theorem icoreresf

Description: Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020)

	Ref	Expression
Assertion	icoreresf	⊢ ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ

Proof

Step	Hyp	Ref	Expression
1		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
2		df-ico	⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
3	2	ixxf	⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
4		ffn	⊢ ( [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → [,) Fn ( ℝ* × ℝ* ) )
5		fnssresb	⊢ ( [,) Fn ( ℝ* × ℝ* ) → ( ( [,) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) ↔ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) ) )
6	3 4 5	mp2b	⊢ ( ( [,) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) ↔ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) )
7	1 6	mpbir	⊢ ( [,) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ )
8		eqid	⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( [,) ↾ ( ℝ × ℝ ) )
9	8	icorempo	⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
10	9	rneqi	⊢ ran ( [,) ↾ ( ℝ × ℝ ) ) = ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
11		ssrab2	⊢ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ ℝ
12		reex	⊢ ℝ ∈ V
13	12	elpw2	⊢ ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ↔ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ ℝ )
14	11 13	mpbir	⊢ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ
15	14	rgen2w	⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ
16		eqid	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
17	16	rnmpo	⊢ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) = { 𝑙 ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } }
18	17	abeq2i	⊢ ( 𝑙 ∈ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
19		simpl	⊢ ( ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ )
20		simpr	⊢ ( ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
21	19 20	r19.29d2r	⊢ ( ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) )
22		eleq1	⊢ ( 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → ( 𝑙 ∈ 𝒫 ℝ ↔ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ) )
23	22	biimparc	⊢ ( ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → 𝑙 ∈ 𝒫 ℝ )
24	23	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → 𝑙 ∈ 𝒫 ℝ ) )
25	24	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → 𝑙 ∈ 𝒫 ℝ )
26	21 25	syl	⊢ ( ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → 𝑙 ∈ 𝒫 ℝ )
27	26	ex	⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑙 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } → 𝑙 ∈ 𝒫 ℝ ) )
28	18 27	syl5bi	⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ → ( 𝑙 ∈ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) → 𝑙 ∈ 𝒫 ℝ ) )
29	28	ssrdv	⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ → ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ⊆ 𝒫 ℝ )
30	15 29	ax-mp	⊢ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ⊆ 𝒫 ℝ
31	10 30	eqsstri	⊢ ran ( [,) ↾ ( ℝ × ℝ ) ) ⊆ 𝒫 ℝ
32		df-f	⊢ ( ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ ↔ ( ( [,) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) ∧ ran ( [,) ↾ ( ℝ × ℝ ) ) ⊆ 𝒫 ℝ ) )
33	7 31 32	mpbir2an	⊢ ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ