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 
|- ( ph -> X e. Fin )
ioorrnopnxrlem.a 
|- ( ph -> A : X --> RR* )
ioorrnopnxrlem.b 
|- ( ph -> B : X --> RR* )
ioorrnopnxrlem.f 
|- ( ph -> F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
ioorrnopnxrlem.l 
|- L = ( i e. X |-> if ( ( A ` i ) = -oo , ( ( F ` i ) - 1 ) , ( A ` i ) ) )
ioorrnopnxrlem.r 
|- R = ( i e. X |-> if ( ( B ` i ) = +oo , ( ( F ` i ) + 1 ) , ( B ` i ) ) )
ioorrnopnxrlem.v 
|- V = X_ i e. X ( ( L ` i ) (,) ( R ` i ) )
Assertion ioorrnopnxrlem 
|- ( ph -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( F e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )

Proof

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