Theorem elhoi

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

	Ref	Expression
Hypothesis	elhoi.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	elhoi	⊢ ( 𝜑 → ( 𝑌 ∈ ( ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) ↔ ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elhoi.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		ovexd	⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ∈ V )
3		elmapg	⊢ ( ( ( 𝐴 [,) 𝐵 ) ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( 𝑌 ∈ ( ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) ↔ 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) ) )
4	2 1 3	syl2anc	⊢ ( 𝜑 → ( 𝑌 ∈ ( ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) ↔ 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) ) )
5		id	⊢ ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) → 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) )
6		icossxr	⊢ ( 𝐴 [,) 𝐵 ) ⊆ ℝ*
7	6	a1i	⊢ ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ* )
8	5 7	fssd	⊢ ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) → 𝑌 : 𝑋 ⟶ ℝ* )
9		ffvelrn	⊢ ( ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) )
10	9	ralrimiva	⊢ ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) )
11	8 10	jca	⊢ ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) → ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) )
12		ffn	⊢ ( 𝑌 : 𝑋 ⟶ ℝ* → 𝑌 Fn 𝑋 )
13	12	adantr	⊢ ( ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑌 Fn 𝑋 )
14		simpr	⊢ ( ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) )
15	13 14	jca	⊢ ( ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑌 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) )
16		ffnfv	⊢ ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑌 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) )
17	15 16	sylibr	⊢ ( ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) )
18	11 17	impbii	⊢ ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) )
19	18	a1i	⊢ ( 𝜑 → ( 𝑌 : 𝑋 ⟶ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) ) )
20	4 19	bitrd	⊢ ( 𝜑 → ( 𝑌 ∈ ( ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) ↔ ( 𝑌 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 ‘ 𝑥 ) ∈ ( 𝐴 [,) 𝐵 ) ) ) )