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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( ph /\ i e. X ) -> ( L ` i ) e. RR )
72 71 rexrd
 |-  ( ( ph /\ i e. X ) -> ( L ` i ) e. RR* )
73 65 ffvelrnda
 |-  ( ( 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 ) ) ) )