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	$$⊢\phi \to X\in \mathrm{Fin}$$
	ioorrnopnxr.a	$$⊢\phi \to A:X⟶{ℝ}^{*}$$
	ioorrnopnxr.b	$$⊢\phi \to B:X⟶{ℝ}^{*}$$
Assertion	ioorrnopnxr

Proof

Step	Hyp	Ref	Expression
1		ioorrnopnxr.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ioorrnopnxr.a	$$⊢\phi \to A:X⟶{ℝ}^{*}$$
3		ioorrnopnxr.b	$$⊢\phi \to B:X⟶{ℝ}^{*}$$
4		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
5	4	prid2	$$⊢\left\{\varnothing \right\}\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
6	5	a1i	$$⊢X=\varnothing \to \left\{\varnothing \right\}\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
7		ixpeq1	$$⊢X=\varnothing \to \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)=\underset{i\in \varnothing }{⨉}\left(A\left(i\right),B\left(i\right)\right)$$
8		ixp0x	$$⊢\underset{i\in \varnothing }{⨉}\left(A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
9	8	a1i	$$⊢X=\varnothing \to \underset{i\in \varnothing }{⨉}\left(A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
10	7 9	eqtrd	$$⊢X=\varnothing \to \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
11		2fveq3
12		rrxtopn0b
13	12	a1i
14	11 13	eqtrd
15	10 14	eleq12d
16	6 15	mpbird
17	16	adantl
18		neqne	$$⊢\neg X=\varnothing \to X\ne \varnothing$$
19	18	adantl	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to X\ne \varnothing$$
20		fveq2	$$⊢i=j\to A\left(i\right)=A\left(j\right)$$
21		fveq2	$$⊢i=j\to B\left(i\right)=B\left(j\right)$$
22	20 21	oveq12d	$$⊢i=j\to \left(A\left(i\right),B\left(i\right)\right)=\left(A\left(j\right),B\left(j\right)\right)$$
23	22	cbvixpv	$$⊢\underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)=\underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
24	23	eleq2i	$$⊢f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\leftrightarrow f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
25	24	biimpi	$$⊢f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\to f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
26	25	adantl	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\right)\to f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)$$
27	1	ad2antrr	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to X\in \mathrm{Fin}$$
28	2	ad2antrr	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to A:X⟶{ℝ}^{*}$$
29	3	ad2antrr	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to B:X⟶{ℝ}^{*}$$
30	24	biimpri	$$⊢f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\to f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)$$
31	30	adantl	$$⊢\left(\left(\phi \wedge X\ne \varnothing \right)\wedge f\in \underset{j\in X}{⨉}\left(A\left(j\right),B\left(j\right)\right)\right)\to f\in \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)$$
32		fveq2	$$⊢j=i\to A\left(j\right)=A\left(i\right)$$
33	32	eqeq1d	$$⊢j=i\to \left(A\left(j\right)=\mathrm{-\infty }\leftrightarrow A\left(i\right)=\mathrm{-\infty }\right)$$
34		fveq2	$$⊢j=i\to f\left(j\right)=f\left(i\right)$$
35	34	oveq1d	$$⊢j=i\to f\left(j\right)-1=f\left(i\right)-1$$
36	33 35 32	ifbieq12d	$$⊢j=i\to if\left(A\left(j\right)=\mathrm{-\infty },f\left(j\right)-1,A\left(j\right)\right)=if\left(A\left(i\right)=\mathrm{-\infty },f\left(i\right)-1,A\left(i\right)\right)$$
37	36	cbvmptv	$$⊢\left(j\in X⟼if\left(A\left(j\right)=\mathrm{-\infty },f\left(j\right)-1,A\left(j\right)\right)\right)=\left(i\in X⟼if\left(A\left(i\right)=\mathrm{-\infty },f\left(i\right)-1,A\left(i\right)\right)\right)$$
38		fveq2	$$⊢j=i\to B\left(j\right)=B\left(i\right)$$
39	38	eqeq1d	$$⊢j=i\to \left(B\left(j\right)=\mathrm{+\infty }\leftrightarrow B\left(i\right)=\mathrm{+\infty }\right)$$
40	34	oveq1d	$$⊢j=i\to f\left(j\right)+1=f\left(i\right)+1$$
41	39 40 38	ifbieq12d	$$⊢j=i\to if\left(B\left(j\right)=\mathrm{+\infty },f\left(j\right)+1,B\left(j\right)\right)=if\left(B\left(i\right)=\mathrm{+\infty },f\left(i\right)+1,B\left(i\right)\right)$$
42	41	cbvmptv	$$⊢\left(j\in X⟼if\left(B\left(j\right)=\mathrm{+\infty },f\left(j\right)+1,B\left(j\right)\right)\right)=\left(i\in X⟼if\left(B\left(i\right)=\mathrm{+\infty },f\left(i\right)+1,B\left(i\right)\right)\right)$$
43		eqid	$$⊢\underset{i\in X}{⨉}\left(\left(j\in X⟼if\left(A\left(j\right)=\mathrm{-\infty },f\left(j\right)-1,A\left(j\right)\right)\right)\left(i\right),\left(j\in X⟼if\left(B\left(j\right)=\mathrm{+\infty },f\left(j\right)+1,B\left(j\right)\right)\right)\left(i\right)\right)=\underset{i\in X}{⨉}\left(\left(j\in X⟼if\left(A\left(j\right)=\mathrm{-\infty },f\left(j\right)-1,A\left(j\right)\right)\right)\left(i\right),\left(j\in X⟼if\left(B\left(j\right)=\mathrm{+\infty },f\left(j\right)+1,B\left(j\right)\right)\right)\left(i\right)\right)$$
44	27 28 29 31 37 42 43	ioorrnopnxrlem
45	26 44	syldan
46	45	ralrimiva
47		eqid
48	47	rrxtop
49	1 48	syl
50	49	adantr
51		eltop2
52	50 51	syl
53	46 52	mpbird
54	19 53	syldan
55	17 54	pm2.61dan