Metamath Proof Explorer

Theorem i0oii

Description: ( 0 [,) A ) is open in II . (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Assertion i0oii 
|- ( A <_ 1 -> ( 0 [,) A ) e. II )

Proof

Step Hyp Ref Expression
1 anandi3r 
 |-  ( ( x e. RR /\ A <_ 1 /\ x < A ) <-> ( ( x e. RR /\ A <_ 1 ) /\ ( x < A /\ A <_ 1 ) ) )
2 rexr 
 |-  ( x e. RR -> x e. RR* )
3 lerelxr 
 |-  <_ C_ ( RR* X. RR* )
4 3 brel 
 |-  ( A <_ 1 -> ( A e. RR* /\ 1 e. RR* ) )
5 4 simpld 
 |-  ( A <_ 1 -> A e. RR* )
6 1xr 
 |-  1 e. RR*
7 xrltletr 
 |-  ( ( x e. RR* /\ A e. RR* /\ 1 e. RR* ) -> ( ( x < A /\ A <_ 1 ) -> x < 1 ) )
8 xrltle 
 |-  ( ( x e. RR* /\ 1 e. RR* ) -> ( x < 1 -> x <_ 1 ) )
9 8 3adant2 
 |-  ( ( x e. RR* /\ A e. RR* /\ 1 e. RR* ) -> ( x < 1 -> x <_ 1 ) )
10 7 9 syld 
 |-  ( ( x e. RR* /\ A e. RR* /\ 1 e. RR* ) -> ( ( x < A /\ A <_ 1 ) -> x <_ 1 ) )
11 6 10 mp3an3 
 |-  ( ( x e. RR* /\ A e. RR* ) -> ( ( x < A /\ A <_ 1 ) -> x <_ 1 ) )
12 2 5 11 syl2an 
 |-  ( ( x e. RR /\ A <_ 1 ) -> ( ( x < A /\ A <_ 1 ) -> x <_ 1 ) )
13 12 imp 
 |-  ( ( ( x e. RR /\ A <_ 1 ) /\ ( x < A /\ A <_ 1 ) ) -> x <_ 1 )
14 1 13 sylbi 
 |-  ( ( x e. RR /\ A <_ 1 /\ x < A ) -> x <_ 1 )
15 14 3com12 
 |-  ( ( A <_ 1 /\ x e. RR /\ x < A ) -> x <_ 1 )
16 15 3expib 
 |-  ( A <_ 1 -> ( ( x e. RR /\ x < A ) -> x <_ 1 ) )
17 16 pm4.71d 
 |-  ( A <_ 1 -> ( ( x e. RR /\ x < A ) <-> ( ( x e. RR /\ x < A ) /\ x <_ 1 ) ) )
18 17 anbi1d 
 |-  ( A <_ 1 -> ( ( ( x e. RR /\ x < A ) /\ 0 <_ x ) <-> ( ( ( x e. RR /\ x < A ) /\ x <_ 1 ) /\ 0 <_ x ) ) )
19 3anan32 
 |-  ( ( x e. RR /\ 0 <_ x /\ x < A ) <-> ( ( x e. RR /\ x < A ) /\ 0 <_ x ) )
20 3anass 
 |-  ( ( x e. RR /\ 0 <_ x /\ x <_ 1 ) <-> ( x e. RR /\ ( 0 <_ x /\ x <_ 1 ) ) )
21 20 anbi2i 
 |-  ( ( ( x e. RR /\ x < A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) <-> ( ( x e. RR /\ x < A ) /\ ( x e. RR /\ ( 0 <_ x /\ x <_ 1 ) ) ) )
22 anandi 
 |-  ( ( x e. RR /\ ( x < A /\ ( 0 <_ x /\ x <_ 1 ) ) ) <-> ( ( x e. RR /\ x < A ) /\ ( x e. RR /\ ( 0 <_ x /\ x <_ 1 ) ) ) )
23 3anass 
 |-  ( ( ( x e. RR /\ x < A ) /\ 0 <_ x /\ x <_ 1 ) <-> ( ( x e. RR /\ x < A ) /\ ( 0 <_ x /\ x <_ 1 ) ) )
24 3anan32 
 |-  ( ( ( x e. RR /\ x < A ) /\ 0 <_ x /\ x <_ 1 ) <-> ( ( ( x e. RR /\ x < A ) /\ x <_ 1 ) /\ 0 <_ x ) )
25 anass 
 |-  ( ( ( x e. RR /\ x < A ) /\ ( 0 <_ x /\ x <_ 1 ) ) <-> ( x e. RR /\ ( x < A /\ ( 0 <_ x /\ x <_ 1 ) ) ) )
26 23 24 25 3bitr3ri 
 |-  ( ( x e. RR /\ ( x < A /\ ( 0 <_ x /\ x <_ 1 ) ) ) <-> ( ( ( x e. RR /\ x < A ) /\ x <_ 1 ) /\ 0 <_ x ) )
27 21 22 26 3bitr2i 
 |-  ( ( ( x e. RR /\ x < A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) <-> ( ( ( x e. RR /\ x < A ) /\ x <_ 1 ) /\ 0 <_ x ) )
28 18 19 27 3bitr4g 
 |-  ( A <_ 1 -> ( ( x e. RR /\ 0 <_ x /\ x < A ) <-> ( ( x e. RR /\ x < A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) ) )
29 0re 
 |-  0 e. RR
30 elico2 
 |-  ( ( 0 e. RR /\ A e. RR* ) -> ( x e. ( 0 [,) A ) <-> ( x e. RR /\ 0 <_ x /\ x < A ) ) )
31 29 5 30 sylancr 
 |-  ( A <_ 1 -> ( x e. ( 0 [,) A ) <-> ( x e. RR /\ 0 <_ x /\ x < A ) ) )
32 elin 
 |-  ( x e. ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) <-> ( x e. ( -oo (,) A ) /\ x e. ( 0 [,] 1 ) ) )
33 elicc01 
 |-  ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
34 33 anbi2i 
 |-  ( ( x e. ( -oo (,) A ) /\ x e. ( 0 [,] 1 ) ) <-> ( x e. ( -oo (,) A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) )
35 32 34 bitri 
 |-  ( x e. ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) <-> ( x e. ( -oo (,) A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) )
36 elioomnf 
 |-  ( A e. RR* -> ( x e. ( -oo (,) A ) <-> ( x e. RR /\ x < A ) ) )
37 5 36 syl 
 |-  ( A <_ 1 -> ( x e. ( -oo (,) A ) <-> ( x e. RR /\ x < A ) ) )
38 37 anbi1d 
 |-  ( A <_ 1 -> ( ( x e. ( -oo (,) A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) <-> ( ( x e. RR /\ x < A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) ) )
39 35 38 syl5bb 
 |-  ( A <_ 1 -> ( x e. ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) <-> ( ( x e. RR /\ x < A ) /\ ( x e. RR /\ 0 <_ x /\ x <_ 1 ) ) ) )
40 28 31 39 3bitr4rd 
 |-  ( A <_ 1 -> ( x e. ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) <-> x e. ( 0 [,) A ) ) )
41 40 eqrdv 
 |-  ( A <_ 1 -> ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) = ( 0 [,) A ) )
42 fvex 
 |-  ( topGen ` ran (,) ) e. _V
43 ovex 
 |-  ( 0 [,] 1 ) e. _V
44 iooretop 
 |-  ( -oo (,) A ) e. ( topGen ` ran (,) )
45 elrestr 
 |-  ( ( ( topGen ` ran (,) ) e. _V /\ ( 0 [,] 1 ) e. _V /\ ( -oo (,) A ) e. ( topGen ` ran (,) ) ) -> ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) )
46 42 43 44 45 mp3an 
 |-  ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
47 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
48 46 47 eleqtrri 
 |-  ( ( -oo (,) A ) i^i ( 0 [,] 1 ) ) e. II
49 41 48 eqeltrrdi 
 |-  ( A <_ 1 -> ( 0 [,) A ) e. II )