Metamath Proof Explorer

Theorem io1ii

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

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

Proof

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