Metamath Proof Explorer

Theorem elicores

Description: Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion elicores ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) )

Proof

Step Hyp Ref Expression
1 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
2 1 reseq1i ⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) )
3 ressxr ⊢ ℝ ⊆ ℝ*
4 resmpo ⊢ ( ( ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ* ) → ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) )
5 3 3 4 mp2an ⊢ ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
6 2 5 eqtri ⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
7 6 rneqi ⊢ ran ( [,) ↾ ( ℝ × ℝ ) ) = ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
8 7 eleq2i ⊢ ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ↔ 𝐴 ∈ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) )
9 eqid ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
10 xrex ⊢ ℝ* ∈ V
11 10 rabex ⊢ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ V
12 9 11 elrnmpo ⊢ ( 𝐴 ∈ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
13 3 sseli ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
14 13 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ* )
15 3 sseli ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
16 15 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ* )
17 icoval ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 [,) 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
18 14 16 17 syl2anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 [,) 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
19 18 eqcomd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } = ( 𝑥 [,) 𝑦 ) )
20 19 eqeq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ↔ 𝐴 = ( 𝑥 [,) 𝑦 ) ) )
21 20 rexbidva ⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑦 ∈ ℝ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ↔ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) ) )
22 21 rexbiia ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) )
23 8 12 22 3bitri ⊢ ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) )