Theorem ioorrnopnxr

Description: The indexed product of open intervals is an open set in ( RR^X ) . Similar to ioorrnopn but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	ioorrnopnxr.x	|- ( ph -> X e. Fin )
	ioorrnopnxr.a	|- ( ph -> A : X --> RR* )
	ioorrnopnxr.b	|- ( ph -> B : X --> RR* )
Assertion	ioorrnopnxr	|- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		ioorrnopnxr.x	|- ( ph -> X e. Fin )
2		ioorrnopnxr.a	|- ( ph -> A : X --> RR* )
3		ioorrnopnxr.b	|- ( ph -> B : X --> RR* )
4		p0ex	|- { (/) } e. _V
5	4	prid2	|- { (/) } e. { (/) , { (/) } }
6	5	a1i	|- ( X = (/) -> { (/) } e. { (/) , { (/) } } )
7		ixpeq1	|- ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) )
8		ixp0x	|- X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) = { (/) }
9	8	a1i	|- ( X = (/) -> X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) = { (/) } )
10	7 9	eqtrd	|- ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = { (/) } )
11		2fveq3	|- ( X = (/) -> ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` (/) ) ) )
12		rrxtopn0b	|- ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } }
13	12	a1i	|- ( X = (/) -> ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } } )
14	11 13	eqtrd	|- ( X = (/) -> ( TopOpen ` ( RR^ ` X ) ) = { (/) , { (/) } } )
15	10 14	eleq12d	|- ( X = (/) -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> { (/) } e. { (/) , { (/) } } ) )
16	6 15	mpbird	|- ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
17	16	adantl	|- ( ( ph /\ X = (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
18		neqne	|- ( -. X = (/) -> X =/= (/) )
19	18	adantl	|- ( ( ph /\ -. X = (/) ) -> X =/= (/) )
20		fveq2	|- ( i = j -> ( A ` i ) = ( A ` j ) )
21		fveq2	|- ( i = j -> ( B ` i ) = ( B ` j ) )
22	20 21	oveq12d	|- ( i = j -> ( ( A ` i ) (,) ( B ` i ) ) = ( ( A ` j ) (,) ( B ` j ) ) )
23	22	cbvixpv	|- X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = X_ j e. X ( ( A ` j ) (,) ( B ` j ) )
24	23	eleq2i	|- ( f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) <-> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
25	24	biimpi	|- ( f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) -> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
26	25	adantl	|- ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
27	1	ad2antrr	|- ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> X e. Fin )
28	2	ad2antrr	|- ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> A : X --> RR* )
29	3	ad2antrr	|- ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> B : X --> RR* )
30	24	biimpri	|- ( f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) -> f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
31	30	adantl	|- ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
32		fveq2	|- ( j = i -> ( A ` j ) = ( A ` i ) )
33	32	eqeq1d	|- ( j = i -> ( ( A ` j ) = -oo <-> ( A ` i ) = -oo ) )
34		fveq2	|- ( j = i -> ( f ` j ) = ( f ` i ) )
35	34	oveq1d	|- ( j = i -> ( ( f ` j ) - 1 ) = ( ( f ` i ) - 1 ) )
36	33 35 32	ifbieq12d	|- ( j = i -> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) = if ( ( A ` i ) = -oo , ( ( f ` i ) - 1 ) , ( A ` i ) ) )
37	36	cbvmptv	|- ( j e. X |-> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) ) = ( i e. X |-> if ( ( A ` i ) = -oo , ( ( f ` i ) - 1 ) , ( A ` i ) ) )
38		fveq2	|- ( j = i -> ( B ` j ) = ( B ` i ) )
39	38	eqeq1d	|- ( j = i -> ( ( B ` j ) = +oo <-> ( B ` i ) = +oo ) )
40	34	oveq1d	|- ( j = i -> ( ( f ` j ) + 1 ) = ( ( f ` i ) + 1 ) )
41	39 40 38	ifbieq12d	|- ( j = i -> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) = if ( ( B ` i ) = +oo , ( ( f ` i ) + 1 ) , ( B ` i ) ) )
42	41	cbvmptv	|- ( j e. X |-> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) ) = ( i e. X |-> if ( ( B ` i ) = +oo , ( ( f ` i ) + 1 ) , ( B ` i ) ) )
43		eqid	|- X_ i e. X ( ( ( j e. X |-> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) ) ` i ) (,) ( ( j e. X |-> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) ) ` i ) ) = X_ i e. X ( ( ( j e. X |-> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) ) ` i ) (,) ( ( j e. X |-> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) ) ` i ) )
44	27 28 29 31 37 42 43	ioorrnopnxrlem	|- ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
45	26 44	syldan	|- ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
46	45	ralrimiva	|- ( ( ph /\ X =/= (/) ) -> A. f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
47		eqid	|- ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` X ) )
48	47	rrxtop	|- ( X e. Fin -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
49	1 48	syl	|- ( ph -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
50	49	adantr	|- ( ( ph /\ X =/= (/) ) -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
51		eltop2	|- ( ( TopOpen ` ( RR^ ` X ) ) e. Top -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> A. f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) ) )
52	50 51	syl	|- ( ( ph /\ X =/= (/) ) -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> A. f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) ) )
53	46 52	mpbird	|- ( ( ph /\ X =/= (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
54	19 53	syldan	|- ( ( ph /\ -. X = (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
55	17 54	pm2.61dan	|- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )