ioorrnopnxrlem

Description: Given a point F that belongs to an indexed product of (possibly unbounded) open intervals, then F belongs to an open product of bounded open intervals that's a subset of the original indexed product. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	ioorrnopnxrlem.x	$⊢ φ \to X \in Fin$
	ioorrnopnxrlem.a	$⊢ φ \to A : X ⟶ ℝ^{*}$
	ioorrnopnxrlem.b	$⊢ φ \to B : X ⟶ ℝ^{*}$
	ioorrnopnxrlem.f	$⊢ φ \to F \in \underset{i \in X}{⨉} (A (i), B (i))$
	ioorrnopnxrlem.l	$⊢ L = (i \in X ⟼ if (A (i) = −∞, F (i) - 1, A (i)))$
	ioorrnopnxrlem.r	$⊢ R = (i \in X ⟼ if (B (i) = +∞, F (i) + 1, B (i)))$
	ioorrnopnxrlem.v	$⊢ V = \underset{i \in X}{⨉} (L (i), R (i))$
Assertion	ioorrnopnxrlem	$⊢ φ \to \exists v \in TopOpen (X) (F \in v \land v \subseteq \underset{i \in X}{⨉} (A (i), B (i)))$

Proof

Step	Hyp	Ref	Expression
1		ioorrnopnxrlem.x	$⊢ φ \to X \in Fin$
2		ioorrnopnxrlem.a	$⊢ φ \to A : X ⟶ ℝ^{*}$
3		ioorrnopnxrlem.b	$⊢ φ \to B : X ⟶ ℝ^{*}$
4		ioorrnopnxrlem.f	$⊢ φ \to F \in \underset{i \in X}{⨉} (A (i), B (i))$
5		ioorrnopnxrlem.l	$⊢ L = (i \in X ⟼ if (A (i) = −∞, F (i) - 1, A (i)))$
6		ioorrnopnxrlem.r	$⊢ R = (i \in X ⟼ if (B (i) = +∞, F (i) + 1, B (i)))$
7		ioorrnopnxrlem.v	$⊢ V = \underset{i \in X}{⨉} (L (i), R (i))$
8	7	a1i	$⊢ φ \to V = \underset{i \in X}{⨉} (L (i), R (i))$
9		iftrue	$⊢ A (i) = −∞ \to if (A (i) = −∞, F (i) - 1, A (i)) = F (i) - 1$
10	9	adantl	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to if (A (i) = −∞, F (i) - 1, A (i)) = F (i) - 1$
11	4	adantr	$⊢ (φ \land i \in X) \to F \in \underset{i \in X}{⨉} (A (i), B (i))$
12		simpr	$⊢ (φ \land i \in X) \to i \in X$
13		fvixp2	$⊢ (F \in \underset{i \in X}{⨉} (A (i), B (i)) \land i \in X) \to F (i) \in (A (i), B (i))$
14	11 12 13	syl2anc	$⊢ (φ \land i \in X) \to F (i) \in (A (i), B (i))$
15	14	elioored	$⊢ (φ \land i \in X) \to F (i) \in ℝ$
16		1red	$⊢ (φ \land i \in X) \to 1 \in ℝ$
17	15 16	resubcld	$⊢ (φ \land i \in X) \to F (i) - 1 \in ℝ$
18	17	adantr	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to F (i) - 1 \in ℝ$
19	10 18	eqeltrd	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to if (A (i) = −∞, F (i) - 1, A (i)) \in ℝ$
20		iffalse	$⊢ \neg A (i) = −∞ \to if (A (i) = −∞, F (i) - 1, A (i)) = A (i)$
21	20	adantl	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to if (A (i) = −∞, F (i) - 1, A (i)) = A (i)$
22		neqne	$⊢ \neg A (i) = −∞ \to A (i) \neq −∞$
23	22	adantl	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to A (i) \neq −∞$
24	2	ffvelcdmda	$⊢ (φ \land i \in X) \to A (i) \in ℝ^{*}$
25	24	adantr	$⊢ ((φ \land i \in X) \land A (i) \neq −∞) \to A (i) \in ℝ^{*}$
26		simpr	$⊢ ((φ \land i \in X) \land A (i) \neq −∞) \to A (i) \neq −∞$
27		pnfxr	$⊢ +∞ \in ℝ^{*}$
28	27	a1i	$⊢ (φ \land i \in X) \to +∞ \in ℝ^{*}$
29	15	rexrd	$⊢ (φ \land i \in X) \to F (i) \in ℝ^{*}$
30	3	ffvelcdmda	$⊢ (φ \land i \in X) \to B (i) \in ℝ^{*}$
31		ioogtlb	$⊢ (A (i) \in ℝ^{} \land B (i) \in ℝ^{} \land F (i) \in (A (i), B (i))) \to A (i) < F (i)$
32	24 30 14 31	syl3anc	$⊢ (φ \land i \in X) \to A (i) < F (i)$
33	15	ltpnfd	$⊢ (φ \land i \in X) \to F (i) < +∞$
34	24 29 28 32 33	xrlttrd	$⊢ (φ \land i \in X) \to A (i) < +∞$
35	24 28 34	xrltned	$⊢ (φ \land i \in X) \to A (i) \neq +∞$
36	35	adantr	$⊢ ((φ \land i \in X) \land A (i) \neq −∞) \to A (i) \neq +∞$
37	25 26 36	xrred	$⊢ ((φ \land i \in X) \land A (i) \neq −∞) \to A (i) \in ℝ$
38	23 37	syldan	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to A (i) \in ℝ$
39	21 38	eqeltrd	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to if (A (i) = −∞, F (i) - 1, A (i)) \in ℝ$
40	19 39	pm2.61dan	$⊢ (φ \land i \in X) \to if (A (i) = −∞, F (i) - 1, A (i)) \in ℝ$
41	40 5	fmptd	$⊢ φ \to L : X ⟶ ℝ$
42		iftrue	$⊢ B (i) = +∞ \to if (B (i) = +∞, F (i) + 1, B (i)) = F (i) + 1$
43	42	adantl	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to if (B (i) = +∞, F (i) + 1, B (i)) = F (i) + 1$
44	15 16	readdcld	$⊢ (φ \land i \in X) \to F (i) + 1 \in ℝ$
45	44	adantr	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to F (i) + 1 \in ℝ$
46	43 45	eqeltrd	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to if (B (i) = +∞, F (i) + 1, B (i)) \in ℝ$
47		iffalse	$⊢ \neg B (i) = +∞ \to if (B (i) = +∞, F (i) + 1, B (i)) = B (i)$
48	47	adantl	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to if (B (i) = +∞, F (i) + 1, B (i)) = B (i)$
49		neqne	$⊢ \neg B (i) = +∞ \to B (i) \neq +∞$
50	49	adantl	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to B (i) \neq +∞$
51	30	adantr	$⊢ ((φ \land i \in X) \land B (i) \neq +∞) \to B (i) \in ℝ^{*}$
52		mnfxr	$⊢ −∞ \in ℝ^{*}$
53	52	a1i	$⊢ (φ \land i \in X) \to −∞ \in ℝ^{*}$
54	15	mnfltd	$⊢ (φ \land i \in X) \to −∞ < F (i)$
55		iooltub	$⊢ (A (i) \in ℝ^{} \land B (i) \in ℝ^{} \land F (i) \in (A (i), B (i))) \to F (i) < B (i)$
56	24 30 14 55	syl3anc	$⊢ (φ \land i \in X) \to F (i) < B (i)$
57	53 29 30 54 56	xrlttrd	$⊢ (φ \land i \in X) \to −∞ < B (i)$
58	53 30 57	xrgtned	$⊢ (φ \land i \in X) \to B (i) \neq −∞$
59	58	adantr	$⊢ ((φ \land i \in X) \land B (i) \neq +∞) \to B (i) \neq −∞$
60		simpr	$⊢ ((φ \land i \in X) \land B (i) \neq +∞) \to B (i) \neq +∞$
61	51 59 60	xrred	$⊢ ((φ \land i \in X) \land B (i) \neq +∞) \to B (i) \in ℝ$
62	50 61	syldan	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to B (i) \in ℝ$
63	48 62	eqeltrd	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to if (B (i) = +∞, F (i) + 1, B (i)) \in ℝ$
64	46 63	pm2.61dan	$⊢ (φ \land i \in X) \to if (B (i) = +∞, F (i) + 1, B (i)) \in ℝ$
65	64 6	fmptd	$⊢ φ \to R : X ⟶ ℝ$
66	1 41 65	ioorrnopn	$⊢ φ \to \underset{i \in X}{⨉} (L (i), R (i)) \in TopOpen (X)$
67	8 66	eqeltrd	$⊢ φ \to V \in TopOpen (X)$
68	4	elexd	$⊢ φ \to F \in V$
69		ixpfn	$⊢ F \in \underset{i \in X}{⨉} (A (i), B (i)) \to F Fn X$
70	4 69	syl	$⊢ φ \to F Fn X$
71	41	ffvelcdmda	$⊢ (φ \land i \in X) \to L (i) \in ℝ$
72	71	rexrd	$⊢ (φ \land i \in X) \to L (i) \in ℝ^{*}$
73	65	ffvelcdmda	$⊢ (φ \land i \in X) \to R (i) \in ℝ$
74	73	rexrd	$⊢ (φ \land i \in X) \to R (i) \in ℝ^{*}$
75	5	a1i	$⊢ φ \to L = (i \in X ⟼ if (A (i) = −∞, F (i) - 1, A (i)))$
76	40	elexd	$⊢ (φ \land i \in X) \to if (A (i) = −∞, F (i) - 1, A (i)) \in V$
77	75 76	fvmpt2d	$⊢ (φ \land i \in X) \to L (i) = if (A (i) = −∞, F (i) - 1, A (i))$
78	77	adantr	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to L (i) = if (A (i) = −∞, F (i) - 1, A (i))$
79	78 10	eqtrd	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to L (i) = F (i) - 1$
80	15	ltm1d	$⊢ (φ \land i \in X) \to F (i) - 1 < F (i)$
81	80	adantr	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to F (i) - 1 < F (i)$
82	79 81	eqbrtrd	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to L (i) < F (i)$
83	77	adantr	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to L (i) = if (A (i) = −∞, F (i) - 1, A (i))$
84	83 21	eqtrd	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to L (i) = A (i)$
85	32	adantr	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to A (i) < F (i)$
86	84 85	eqbrtrd	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to L (i) < F (i)$
87	82 86	pm2.61dan	$⊢ (φ \land i \in X) \to L (i) < F (i)$
88	15	ltp1d	$⊢ (φ \land i \in X) \to F (i) < F (i) + 1$
89	88	adantr	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to F (i) < F (i) + 1$
90	6	a1i	$⊢ φ \to R = (i \in X ⟼ if (B (i) = +∞, F (i) + 1, B (i)))$
91	64	elexd	$⊢ (φ \land i \in X) \to if (B (i) = +∞, F (i) + 1, B (i)) \in V$
92	90 91	fvmpt2d	$⊢ (φ \land i \in X) \to R (i) = if (B (i) = +∞, F (i) + 1, B (i))$
93	92	adantr	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to R (i) = if (B (i) = +∞, F (i) + 1, B (i))$
94	93 43	eqtrd	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to R (i) = F (i) + 1$
95	94	eqcomd	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to F (i) + 1 = R (i)$
96	89 95	breqtrd	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to F (i) < R (i)$
97	56	adantr	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to F (i) < B (i)$
98	92	adantr	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to R (i) = if (B (i) = +∞, F (i) + 1, B (i))$
99	98 48	eqtrd	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to R (i) = B (i)$
100	99	eqcomd	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to B (i) = R (i)$
101	97 100	breqtrd	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to F (i) < R (i)$
102	96 101	pm2.61dan	$⊢ (φ \land i \in X) \to F (i) < R (i)$
103	72 74 15 87 102	eliood	$⊢ (φ \land i \in X) \to F (i) \in (L (i), R (i))$
104	103	ralrimiva	$⊢ φ \to \forall i \in X F (i) \in (L (i), R (i))$
105	68 70 104	3jca	$⊢ φ \to (F \in V \land F Fn X \land \forall i \in X F (i) \in (L (i), R (i)))$
106		elixp2	$⊢ F \in \underset{i \in X}{⨉} (L (i), R (i)) \leftrightarrow (F \in V \land F Fn X \land \forall i \in X F (i) \in (L (i), R (i)))$
107	105 106	sylibr	$⊢ φ \to F \in \underset{i \in X}{⨉} (L (i), R (i))$
108	107 7	eleqtrrdi	$⊢ φ \to F \in V$
109	24	adantr	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to A (i) \in ℝ^{*}$
110	72	adantr	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to L (i) \in ℝ^{*}$
111	19	mnfltd	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to −∞ < if (A (i) = −∞, F (i) - 1, A (i))$
112	111 10	breqtrd	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to −∞ < F (i) - 1$
113		simpr	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to A (i) = −∞$
114	113 79	breq12d	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to (A (i) < L (i) \leftrightarrow −∞ < F (i) - 1)$
115	112 114	mpbird	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to A (i) < L (i)$
116	109 110 115	xrltled	$⊢ ((φ \land i \in X) \land A (i) = −∞) \to A (i) \leq L (i)$
117	84	eqcomd	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to A (i) = L (i)$
118	38 117	eqled	$⊢ ((φ \land i \in X) \land \neg A (i) = −∞) \to A (i) \leq L (i)$
119	116 118	pm2.61dan	$⊢ (φ \land i \in X) \to A (i) \leq L (i)$
120	74	adantr	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to R (i) \in ℝ^{*}$
121	30	adantr	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to B (i) \in ℝ^{*}$
122	45	ltpnfd	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to F (i) + 1 < +∞$
123		simpr	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to B (i) = +∞$
124	94 123	breq12d	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to (R (i) < B (i) \leftrightarrow F (i) + 1 < +∞)$
125	122 124	mpbird	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to R (i) < B (i)$
126	120 121 125	xrltled	$⊢ ((φ \land i \in X) \land B (i) = +∞) \to R (i) \leq B (i)$
127	73	adantr	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to R (i) \in ℝ$
128	127 99	eqled	$⊢ ((φ \land i \in X) \land \neg B (i) = +∞) \to R (i) \leq B (i)$
129	126 128	pm2.61dan	$⊢ (φ \land i \in X) \to R (i) \leq B (i)$
130		ioossioo	$⊢ ((A (i) \in ℝ^{} \land B (i) \in ℝ^{}) \land (A (i) \leq L (i) \land R (i) \leq B (i))) \to (L (i), R (i)) \subseteq (A (i), B (i))$
131	24 30 119 129 130	syl22anc	$⊢ (φ \land i \in X) \to (L (i), R (i)) \subseteq (A (i), B (i))$
132	131	ralrimiva	$⊢ φ \to \forall i \in X (L (i), R (i)) \subseteq (A (i), B (i))$
133		ss2ixp	$⊢ \forall i \in X (L (i), R (i)) \subseteq (A (i), B (i)) \to \underset{i \in X}{⨉} (L (i), R (i)) \subseteq \underset{i \in X}{⨉} (A (i), B (i))$
134	132 133	syl	$⊢ φ \to \underset{i \in X}{⨉} (L (i), R (i)) \subseteq \underset{i \in X}{⨉} (A (i), B (i))$
135	8 134	eqsstrd	$⊢ φ \to V \subseteq \underset{i \in X}{⨉} (A (i), B (i))$
136	108 135	jca	$⊢ φ \to (F \in V \land V \subseteq \underset{i \in X}{⨉} (A (i), B (i)))$
137		eleq2	$⊢ v = V \to (F \in v \leftrightarrow F \in V)$
138		sseq1	$⊢ v = V \to (v \subseteq \underset{i \in X}{⨉} (A (i), B (i)) \leftrightarrow V \subseteq \underset{i \in X}{⨉} (A (i), B (i)))$
139	137 138	anbi12d	$⊢ v = V \to ((F \in v \land v \subseteq \underset{i \in X}{⨉} (A (i), B (i))) \leftrightarrow (F \in V \land V \subseteq \underset{i \in X}{⨉} (A (i), B (i))))$
140	139	rspcev	$⊢ (V \in TopOpen (X) \land (F \in V \land V \subseteq \underset{i \in X}{⨉} (A (i), B (i)))) \to \exists v \in TopOpen (X) (F \in v \land v \subseteq \underset{i \in X}{⨉} (A (i), B (i)))$
141	67 136 140	syl2anc	$⊢ φ \to \exists v \in TopOpen (X) (F \in v \land v \subseteq \underset{i \in X}{⨉} (A (i), B (i)))$

Metamath Proof Explorer

Theorem ioorrnopnxrlem

Proof