Theorem elhoi

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

	Ref	Expression
Hypothesis	elhoi.1	|- ( ph -> X e. V )
Assertion	elhoi	|- ( ph -> ( Y e. ( ( A [,) B ) ^m X ) <-> ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elhoi.1	|- ( ph -> X e. V )
2		ovexd	|- ( ph -> ( A [,) B ) e. _V )
3		elmapg	|- ( ( ( A [,) B ) e. _V /\ X e. V ) -> ( Y e. ( ( A [,) B ) ^m X ) <-> Y : X --> ( A [,) B ) ) )
4	2 1 3	syl2anc	|- ( ph -> ( Y e. ( ( A [,) B ) ^m X ) <-> Y : X --> ( A [,) B ) ) )
5		id	|- ( Y : X --> ( A [,) B ) -> Y : X --> ( A [,) B ) )
6		icossxr	|- ( A [,) B ) C_ RR*
7	6	a1i	|- ( Y : X --> ( A [,) B ) -> ( A [,) B ) C_ RR* )
8	5 7	fssd	|- ( Y : X --> ( A [,) B ) -> Y : X --> RR* )
9		ffvelrn	|- ( ( Y : X --> ( A [,) B ) /\ x e. X ) -> ( Y ` x ) e. ( A [,) B ) )
10	9	ralrimiva	|- ( Y : X --> ( A [,) B ) -> A. x e. X ( Y ` x ) e. ( A [,) B ) )
11	8 10	jca	|- ( Y : X --> ( A [,) B ) -> ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) )
12		ffn	|- ( Y : X --> RR* -> Y Fn X )
13	12	adantr	|- ( ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) -> Y Fn X )
14		simpr	|- ( ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) -> A. x e. X ( Y ` x ) e. ( A [,) B ) )
15	13 14	jca	|- ( ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) -> ( Y Fn X /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) )
16		ffnfv	|- ( Y : X --> ( A [,) B ) <-> ( Y Fn X /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) )
17	15 16	sylibr	|- ( ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) -> Y : X --> ( A [,) B ) )
18	11 17	impbii	|- ( Y : X --> ( A [,) B ) <-> ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) )
19	18	a1i	|- ( ph -> ( Y : X --> ( A [,) B ) <-> ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) ) )
20	4 19	bitrd	|- ( ph -> ( Y e. ( ( A [,) B ) ^m X ) <-> ( Y : X --> RR* /\ A. x e. X ( Y ` x ) e. ( A [,) B ) ) ) )