Metamath Proof Explorer


Theorem 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 φ X Fin
ioorrnopnxrlem.a φ A : X *
ioorrnopnxrlem.b φ B : X *
ioorrnopnxrlem.f φ F i X A i B i
ioorrnopnxrlem.l L = i X if A i = −∞ F i 1 A i
ioorrnopnxrlem.r R = i X if B i = +∞ F i + 1 B i
ioorrnopnxrlem.v V = i X L i R i
Assertion ioorrnopnxrlem φ v TopOpen X F v v i X A i B i

Proof

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