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	bilani	$$⊢\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)$$
26	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}$$
27	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⟶{ℝ}^{*}$$
28	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⟶{ℝ}^{*}$$
29	24	bilanri	$$⊢\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)$$
30		fveq2	$$⊢j=i\to A\left(j\right)=A\left(i\right)$$
31	30	eqeq1d	$$⊢j=i\to \left(A\left(j\right)=\mathrm{-\infty }\leftrightarrow A\left(i\right)=\mathrm{-\infty }\right)$$
32		fveq2	$$⊢j=i\to f\left(j\right)=f\left(i\right)$$
33	32	oveq1d	$$⊢j=i\to f\left(j\right)-1=f\left(i\right)-1$$
34	31 33 30	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)$$
35	34	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)$$
36		fveq2	$$⊢j=i\to B\left(j\right)=B\left(i\right)$$
37	36	eqeq1d	$$⊢j=i\to \left(B\left(j\right)=\mathrm{+\infty }\leftrightarrow B\left(i\right)=\mathrm{+\infty }\right)$$
38	32	oveq1d	$$⊢j=i\to f\left(j\right)+1=f\left(i\right)+1$$
39	37 38 36	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)$$
40	39	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)$$
41		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)$$
42	26 27 28 29 35 40 41	ioorrnopnxrlem
43	25 42	syldan
44	43	ralrimiva
45		eqid
46	45	rrxtop
47	1 46	syl
48	47	adantr
49		eltop2
50	48 49	syl
51	44 50	mpbird
52	19 51	syldan
53	17 52	pm2.61dan