# Metamath Proof Explorer

## Theorem elhoi

Description: Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis elhoi.1 $⊢ φ → X ∈ V$
Assertion elhoi $⊢ φ → Y ∈ A B X ↔ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B$

### Proof

Step Hyp Ref Expression
1 elhoi.1 $⊢ φ → X ∈ V$
2 ovexd $⊢ φ → A B ∈ V$
3 elmapg $⊢ A B ∈ V ∧ X ∈ V → Y ∈ A B X ↔ Y : X ⟶ A B$
4 2 1 3 syl2anc $⊢ φ → Y ∈ A B X ↔ Y : X ⟶ A B$
5 id $⊢ Y : X ⟶ A B → Y : X ⟶ A B$
6 icossxr $⊢ A B ⊆ ℝ *$
7 6 a1i $⊢ Y : X ⟶ A B → A B ⊆ ℝ *$
8 5 7 fssd $⊢ Y : X ⟶ A B → Y : X ⟶ ℝ *$
9 ffvelrn $⊢ Y : X ⟶ A B ∧ x ∈ X → Y ⁡ x ∈ A B$
10 9 ralrimiva $⊢ Y : X ⟶ A B → ∀ x ∈ X Y ⁡ x ∈ A B$
11 8 10 jca $⊢ Y : X ⟶ A B → Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B$
12 ffn $⊢ Y : X ⟶ ℝ * → Y Fn X$
13 12 adantr $⊢ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B → Y Fn X$
14 simpr $⊢ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B → ∀ x ∈ X Y ⁡ x ∈ A B$
15 13 14 jca $⊢ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B → Y Fn X ∧ ∀ x ∈ X Y ⁡ x ∈ A B$
16 ffnfv $⊢ Y : X ⟶ A B ↔ Y Fn X ∧ ∀ x ∈ X Y ⁡ x ∈ A B$
17 15 16 sylibr $⊢ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B → Y : X ⟶ A B$
18 11 17 impbii $⊢ Y : X ⟶ A B ↔ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B$
19 18 a1i $⊢ φ → Y : X ⟶ A B ↔ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B$
20 4 19 bitrd $⊢ φ → Y ∈ A B X ↔ Y : X ⟶ ℝ * ∧ ∀ x ∈ X Y ⁡ x ∈ A B$