Step |
Hyp |
Ref |
Expression |
1 |
|
eqidd |
⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) |
2 |
|
ssrab2 |
⊢ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ ℝ* |
3 |
|
xrex |
⊢ ℝ* ∈ V |
4 |
3
|
rabex |
⊢ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ V |
5 |
4
|
elpw |
⊢ ( { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* ↔ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ ℝ* ) |
6 |
2 5
|
mpbir |
⊢ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* |
7 |
1 6
|
eqeltrrdi |
⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* ) |
8 |
7
|
rgen2 |
⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* |
9 |
|
df-ico |
⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ) |
10 |
9
|
fmpo |
⊢ ( ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* ↔ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* ) |
11 |
8 10
|
mpbi |
⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* |