Metamath Proof Explorer

Theorem iooii

Description: Open intervals are open sets of II . (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Assertion iooii 
|- ( ( 0 <_ A /\ B <_ 1 ) -> ( A (,) B ) e. II )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 1xr 
 |-  1 e. RR*
3 ioossioo 
 |-  ( ( ( 0 e. RR* /\ 1 e. RR* ) /\ ( 0 <_ A /\ B <_ 1 ) ) -> ( A (,) B ) C_ ( 0 (,) 1 ) )
4 1 2 3 mpanl12 
 |-  ( ( 0 <_ A /\ B <_ 1 ) -> ( A (,) B ) C_ ( 0 (,) 1 ) )
5 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
6 iooretop 
 |-  ( 0 (,) 1 ) e. ( topGen ` ran (,) )
7 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
8 retop 
 |-  ( topGen ` ran (,) ) e. Top
9 ovex 
 |-  ( 0 [,] 1 ) e. _V
10 restopnb 
 |-  ( ( ( ( topGen ` ran (,) ) e. Top /\ ( 0 [,] 1 ) e. _V ) /\ ( ( 0 (,) 1 ) e. ( topGen ` ran (,) ) /\ ( 0 (,) 1 ) C_ ( 0 [,] 1 ) /\ ( A (,) B ) C_ ( 0 (,) 1 ) ) ) -> ( ( A (,) B ) e. ( topGen ` ran (,) ) <-> ( A (,) B ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) ) )
11 8 9 10 mpanl12 
 |-  ( ( ( 0 (,) 1 ) e. ( topGen ` ran (,) ) /\ ( 0 (,) 1 ) C_ ( 0 [,] 1 ) /\ ( A (,) B ) C_ ( 0 (,) 1 ) ) -> ( ( A (,) B ) e. ( topGen ` ran (,) ) <-> ( A (,) B ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) ) )
12 6 7 11 mp3an12 
 |-  ( ( A (,) B ) C_ ( 0 (,) 1 ) -> ( ( A (,) B ) e. ( topGen ` ran (,) ) <-> ( A (,) B ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) ) )
13 5 12 mpbii 
 |-  ( ( A (,) B ) C_ ( 0 (,) 1 ) -> ( A (,) B ) e. ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) )
14 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
15 13 14 eleqtrrdi 
 |-  ( ( A (,) B ) C_ ( 0 (,) 1 ) -> ( A (,) B ) e. II )
16 4 15 syl 
 |-  ( ( 0 <_ A /\ B <_ 1 ) -> ( A (,) B ) e. II )