elhoi

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

		Ref	Expression
	Hypothesis	elhoi.1	$⊢ φ \to X \in V$
	Assertion	elhoi	$⊢ φ \to (Y \in ({[A, B)}^{X}) \leftrightarrow (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B)))$

Proof

Step	Hyp	Ref	Expression
1		elhoi.1	$⊢ φ \to X \in V$
2		ovexd	$⊢ φ \to [A, B) \in V$
3		elmapg	$⊢ ([A, B) \in V \land X \in V) \to (Y \in ({[A, B)}^{X}) \leftrightarrow Y : X ⟶ [A, B))$
4	2 1 3	syl2anc	$⊢ φ \to (Y \in ({[A, B)}^{X}) \leftrightarrow Y : X ⟶ [A, B))$
5		id	$⊢ Y : X ⟶ [A, B) \to Y : X ⟶ [A, B)$
6		icossxr	$⊢ [A, B) \subseteq ℝ^{*}$
7	6	a1i	$⊢ Y : X ⟶ [A, B) \to [A, B) \subseteq ℝ^{*}$
8	5 7	fssd	$⊢ Y : X ⟶ [A, B) \to Y : X ⟶ ℝ^{*}$
9		ffvelrn	$⊢ (Y : X ⟶ [A, B) \land x \in X) \to Y (x) \in [A, B)$
10	9	ralrimiva	$⊢ Y : X ⟶ [A, B) \to \forall x \in X Y (x) \in [A, B)$
11	8 10	jca	$⊢ Y : X ⟶ [A, B) \to (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B))$
12		ffn	$⊢ Y : X ⟶ ℝ^{*} \to Y Fn X$
13	12	adantr	$⊢ (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B)) \to Y Fn X$
14		simpr	$⊢ (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B)) \to \forall x \in X Y (x) \in [A, B)$
15	13 14	jca	$⊢ (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B)) \to (Y Fn X \land \forall x \in X Y (x) \in [A, B))$
16		ffnfv	$⊢ Y : X ⟶ [A, B) \leftrightarrow (Y Fn X \land \forall x \in X Y (x) \in [A, B))$
17	15 16	sylibr	$⊢ (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B)) \to Y : X ⟶ [A, B)$
18	11 17	impbii	$⊢ Y : X ⟶ [A, B) \leftrightarrow (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B))$
19	18	a1i	$⊢ φ \to (Y : X ⟶ [A, B) \leftrightarrow (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B)))$
20	4 19	bitrd	$⊢ φ \to (Y \in ({[A, B)}^{X}) \leftrightarrow (Y : X ⟶ ℝ^{*} \land \forall x \in X Y (x) \in [A, B)))$

Metamath Proof Explorer

Theorem elhoi

Proof