Metamath Proof Explorer

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 
|- ( ph -> X e. Fin )
ioorrnopnxr.a 
|- ( ph -> A : X --> RR* )
ioorrnopnxr.b 
|- ( ph -> B : X --> RR* )
Assertion ioorrnopnxr 
|- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )

Proof

Step Hyp Ref Expression
1 ioorrnopnxr.x 
 |-  ( ph -> X e. Fin )
2 ioorrnopnxr.a 
 |-  ( ph -> A : X --> RR* )
3 ioorrnopnxr.b 
 |-  ( ph -> B : X --> RR* )
4 p0ex 
 |-  { (/) } e. _V
5 4 prid2 
 |-  { (/) } e. { (/) , { (/) } }
6 5 a1i 
 |-  ( X = (/) -> { (/) } e. { (/) , { (/) } } )
7 ixpeq1 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) )
8 ixp0x 
 |-  X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) = { (/) }
9 8 a1i 
 |-  ( X = (/) -> X_ i e. (/) ( ( A ` i ) (,) ( B ` i ) ) = { (/) } )
10 7 9 eqtrd 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = { (/) } )
11 2fveq3 
 |-  ( X = (/) -> ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` (/) ) ) )
12 rrxtopn0b 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } }
13 12 a1i 
 |-  ( X = (/) -> ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } } )
14 11 13 eqtrd 
 |-  ( X = (/) -> ( TopOpen ` ( RR^ ` X ) ) = { (/) , { (/) } } )
15 10 14 eleq12d 
 |-  ( X = (/) -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> { (/) } e. { (/) , { (/) } } ) )
16 6 15 mpbird 
 |-  ( X = (/) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
17 16 adantl 
 |-  ( ( ph /\ X = (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
18 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
19 18 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
20 fveq2 
 |-  ( i = j -> ( A ` i ) = ( A ` j ) )
21 fveq2 
 |-  ( i = j -> ( B ` i ) = ( B ` j ) )
22 20 21 oveq12d 
 |-  ( i = j -> ( ( A ` i ) (,) ( B ` i ) ) = ( ( A ` j ) (,) ( B ` j ) ) )
23 22 cbvixpv 
 |-  X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) = X_ j e. X ( ( A ` j ) (,) ( B ` j ) )
24 23 eleq2i 
 |-  ( f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) <-> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
25 24 bilani 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) -> f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) )
26 1 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> X e. Fin )
27 2 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> A : X --> RR* )
28 3 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> B : X --> RR* )
29 24 bilanri 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> f e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
30 fveq2 
 |-  ( j = i -> ( A ` j ) = ( A ` i ) )
31 30 eqeq1d 
 |-  ( j = i -> ( ( A ` j ) = -oo <-> ( A ` i ) = -oo ) )
32 fveq2 
 |-  ( j = i -> ( f ` j ) = ( f ` i ) )
33 32 oveq1d 
 |-  ( j = i -> ( ( f ` j ) - 1 ) = ( ( f ` i ) - 1 ) )
34 31 33 30 ifbieq12d 
 |-  ( j = i -> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) = if ( ( A ` i ) = -oo , ( ( f ` i ) - 1 ) , ( A ` i ) ) )
35 34 cbvmptv 
 |-  ( j e. X |-> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) ) = ( i e. X |-> if ( ( A ` i ) = -oo , ( ( f ` i ) - 1 ) , ( A ` i ) ) )
36 fveq2 
 |-  ( j = i -> ( B ` j ) = ( B ` i ) )
37 36 eqeq1d 
 |-  ( j = i -> ( ( B ` j ) = +oo <-> ( B ` i ) = +oo ) )
38 32 oveq1d 
 |-  ( j = i -> ( ( f ` j ) + 1 ) = ( ( f ` i ) + 1 ) )
39 37 38 36 ifbieq12d 
 |-  ( j = i -> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) = if ( ( B ` i ) = +oo , ( ( f ` i ) + 1 ) , ( B ` i ) ) )
40 39 cbvmptv 
 |-  ( j e. X |-> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) ) = ( i e. X |-> if ( ( B ` i ) = +oo , ( ( f ` i ) + 1 ) , ( B ` i ) ) )
41 eqid 
 |-  X_ i e. X ( ( ( j e. X |-> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) ) ` i ) (,) ( ( j e. X |-> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) ) ` i ) ) = X_ i e. X ( ( ( j e. X |-> if ( ( A ` j ) = -oo , ( ( f ` j ) - 1 ) , ( A ` j ) ) ) ` i ) (,) ( ( j e. X |-> if ( ( B ` j ) = +oo , ( ( f ` j ) + 1 ) , ( B ` j ) ) ) ` i ) )
42 26 27 28 29 35 40 41 ioorrnopnxrlem 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. X_ j e. X ( ( A ` j ) (,) ( B ` j ) ) ) -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( f e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
43 25 42 syldan 
 |-  ( ( ( ph /\ X =/= (/) ) /\ f e. 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 ) ) ) )
44 43 ralrimiva 
 |-  ( ( ph /\ X =/= (/) ) -> A. f e. 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 ) ) ) )
45 eqid 
 |-  ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` X ) )
46 45 rrxtop 
 |-  ( X e. Fin -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
47 1 46 syl 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
48 47 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( TopOpen ` ( RR^ ` X ) ) e. Top )
49 eltop2 
 |-  ( ( TopOpen ` ( RR^ ` X ) ) e. Top -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> A. f e. 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 ) ) ) ) )
50 48 49 syl 
 |-  ( ( ph /\ X =/= (/) ) -> ( X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) <-> A. f e. 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 ) ) ) ) )
51 44 50 mpbird 
 |-  ( ( ph /\ X =/= (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
52 19 51 syldan 
 |-  ( ( ph /\ -. X = (/) ) -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
53 17 52 pm2.61dan 
 |-  ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )