Metamath Proof Explorer

Theorem qtopbaslem

Description: The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypothesis qtopbas.1 
|- S C_ RR*
Assertion qtopbaslem 
|- ( (,) " ( S X. S ) ) e. TopBases

Proof

Step Hyp Ref Expression
1 qtopbas.1 
 |-  S C_ RR*
2 iooex 
 |-  (,) e. _V
3 2 imaex 
 |-  ( (,) " ( S X. S ) ) e. _V
4 1 sseli 
 |-  ( z e. S -> z e. RR* )
5 1 sseli 
 |-  ( w e. S -> w e. RR* )
6 4 5 anim12i 
 |-  ( ( z e. S /\ w e. S ) -> ( z e. RR* /\ w e. RR* ) )
7 1 sseli 
 |-  ( v e. S -> v e. RR* )
8 1 sseli 
 |-  ( u e. S -> u e. RR* )
9 7 8 anim12i 
 |-  ( ( v e. S /\ u e. S ) -> ( v e. RR* /\ u e. RR* ) )
10 iooin 
 |-  ( ( ( z e. RR* /\ w e. RR* ) /\ ( v e. RR* /\ u e. RR* ) ) -> ( ( z (,) w ) i^i ( v (,) u ) ) = ( if ( z <_ v , v , z ) (,) if ( w <_ u , w , u ) ) )
11 6 9 10 syl2an 
 |-  ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( ( z (,) w ) i^i ( v (,) u ) ) = ( if ( z <_ v , v , z ) (,) if ( w <_ u , w , u ) ) )
12 ifcl 
 |-  ( ( v e. S /\ z e. S ) -> if ( z <_ v , v , z ) e. S )
13 12 ancoms 
 |-  ( ( z e. S /\ v e. S ) -> if ( z <_ v , v , z ) e. S )
14 ifcl 
 |-  ( ( w e. S /\ u e. S ) -> if ( w <_ u , w , u ) e. S )
15 df-ov 
 |-  ( if ( z <_ v , v , z ) (,) if ( w <_ u , w , u ) ) = ( (,) ` <. if ( z <_ v , v , z ) , if ( w <_ u , w , u ) >. )
16 opelxpi 
 |-  ( ( if ( z <_ v , v , z ) e. S /\ if ( w <_ u , w , u ) e. S ) -> <. if ( z <_ v , v , z ) , if ( w <_ u , w , u ) >. e. ( S X. S ) )
17 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
18 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
19 17 18 ax-mp 
 |-  Fun (,)
20 xpss12 
 |-  ( ( S C_ RR* /\ S C_ RR* ) -> ( S X. S ) C_ ( RR* X. RR* ) )
21 1 1 20 mp2an 
 |-  ( S X. S ) C_ ( RR* X. RR* )
22 17 fdmi 
 |-  dom (,) = ( RR* X. RR* )
23 21 22 sseqtrri 
 |-  ( S X. S ) C_ dom (,)
24 funfvima2 
 |-  ( ( Fun (,) /\ ( S X. S ) C_ dom (,) ) -> ( <. if ( z <_ v , v , z ) , if ( w <_ u , w , u ) >. e. ( S X. S ) -> ( (,) ` <. if ( z <_ v , v , z ) , if ( w <_ u , w , u ) >. ) e. ( (,) " ( S X. S ) ) ) )
25 19 23 24 mp2an 
 |-  ( <. if ( z <_ v , v , z ) , if ( w <_ u , w , u ) >. e. ( S X. S ) -> ( (,) ` <. if ( z <_ v , v , z ) , if ( w <_ u , w , u ) >. ) e. ( (,) " ( S X. S ) ) )
26 16 25 syl 
 |-  ( ( if ( z <_ v , v , z ) e. S /\ if ( w <_ u , w , u ) e. S ) -> ( (,) ` <. if ( z <_ v , v , z ) , if ( w <_ u , w , u ) >. ) e. ( (,) " ( S X. S ) ) )
27 15 26 eqeltrid 
 |-  ( ( if ( z <_ v , v , z ) e. S /\ if ( w <_ u , w , u ) e. S ) -> ( if ( z <_ v , v , z ) (,) if ( w <_ u , w , u ) ) e. ( (,) " ( S X. S ) ) )
28 13 14 27 syl2an 
 |-  ( ( ( z e. S /\ v e. S ) /\ ( w e. S /\ u e. S ) ) -> ( if ( z <_ v , v , z ) (,) if ( w <_ u , w , u ) ) e. ( (,) " ( S X. S ) ) )
29 28 an4s 
 |-  ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( if ( z <_ v , v , z ) (,) if ( w <_ u , w , u ) ) e. ( (,) " ( S X. S ) ) )
30 11 29 eqeltrd 
 |-  ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) )
31 30 ralrimivva 
 |-  ( ( z e. S /\ w e. S ) -> A. v e. S A. u e. S ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) )
32 31 rgen2 
 |-  A. z e. S A. w e. S A. v e. S A. u e. S ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) )
33 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
34 17 33 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
35 ineq1 
 |-  ( x = ( (,) ` t ) -> ( x i^i y ) = ( ( (,) ` t ) i^i y ) )
36 35 eleq1d 
 |-  ( x = ( (,) ` t ) -> ( ( x i^i y ) e. ( (,) " ( S X. S ) ) <-> ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) ) )
37 36 ralbidv 
 |-  ( x = ( (,) ` t ) -> ( A. y e. ( (,) " ( S X. S ) ) ( x i^i y ) e. ( (,) " ( S X. S ) ) <-> A. y e. ( (,) " ( S X. S ) ) ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) ) )
38 37 ralima 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ ( S X. S ) C_ ( RR* X. RR* ) ) -> ( A. x e. ( (,) " ( S X. S ) ) A. y e. ( (,) " ( S X. S ) ) ( x i^i y ) e. ( (,) " ( S X. S ) ) <-> A. t e. ( S X. S ) A. y e. ( (,) " ( S X. S ) ) ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) ) )
39 34 21 38 mp2an 
 |-  ( A. x e. ( (,) " ( S X. S ) ) A. y e. ( (,) " ( S X. S ) ) ( x i^i y ) e. ( (,) " ( S X. S ) ) <-> A. t e. ( S X. S ) A. y e. ( (,) " ( S X. S ) ) ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) )
40 fveq2 
 |-  ( t = <. z , w >. -> ( (,) ` t ) = ( (,) ` <. z , w >. ) )
41 df-ov 
 |-  ( z (,) w ) = ( (,) ` <. z , w >. )
42 40 41 eqtr4di 
 |-  ( t = <. z , w >. -> ( (,) ` t ) = ( z (,) w ) )
43 42 ineq1d 
 |-  ( t = <. z , w >. -> ( ( (,) ` t ) i^i y ) = ( ( z (,) w ) i^i y ) )
44 43 eleq1d 
 |-  ( t = <. z , w >. -> ( ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) <-> ( ( z (,) w ) i^i y ) e. ( (,) " ( S X. S ) ) ) )
45 44 ralbidv 
 |-  ( t = <. z , w >. -> ( A. y e. ( (,) " ( S X. S ) ) ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) <-> A. y e. ( (,) " ( S X. S ) ) ( ( z (,) w ) i^i y ) e. ( (,) " ( S X. S ) ) ) )
46 ineq2 
 |-  ( y = ( (,) ` t ) -> ( ( z (,) w ) i^i y ) = ( ( z (,) w ) i^i ( (,) ` t ) ) )
47 46 eleq1d 
 |-  ( y = ( (,) ` t ) -> ( ( ( z (,) w ) i^i y ) e. ( (,) " ( S X. S ) ) <-> ( ( z (,) w ) i^i ( (,) ` t ) ) e. ( (,) " ( S X. S ) ) ) )
48 47 ralima 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ ( S X. S ) C_ ( RR* X. RR* ) ) -> ( A. y e. ( (,) " ( S X. S ) ) ( ( z (,) w ) i^i y ) e. ( (,) " ( S X. S ) ) <-> A. t e. ( S X. S ) ( ( z (,) w ) i^i ( (,) ` t ) ) e. ( (,) " ( S X. S ) ) ) )
49 34 21 48 mp2an 
 |-  ( A. y e. ( (,) " ( S X. S ) ) ( ( z (,) w ) i^i y ) e. ( (,) " ( S X. S ) ) <-> A. t e. ( S X. S ) ( ( z (,) w ) i^i ( (,) ` t ) ) e. ( (,) " ( S X. S ) ) )
50 fveq2 
 |-  ( t = <. v , u >. -> ( (,) ` t ) = ( (,) ` <. v , u >. ) )
51 df-ov 
 |-  ( v (,) u ) = ( (,) ` <. v , u >. )
52 50 51 eqtr4di 
 |-  ( t = <. v , u >. -> ( (,) ` t ) = ( v (,) u ) )
53 52 ineq2d 
 |-  ( t = <. v , u >. -> ( ( z (,) w ) i^i ( (,) ` t ) ) = ( ( z (,) w ) i^i ( v (,) u ) ) )
54 53 eleq1d 
 |-  ( t = <. v , u >. -> ( ( ( z (,) w ) i^i ( (,) ` t ) ) e. ( (,) " ( S X. S ) ) <-> ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) ) )
55 54 ralxp 
 |-  ( A. t e. ( S X. S ) ( ( z (,) w ) i^i ( (,) ` t ) ) e. ( (,) " ( S X. S ) ) <-> A. v e. S A. u e. S ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) )
56 49 55 bitri 
 |-  ( A. y e. ( (,) " ( S X. S ) ) ( ( z (,) w ) i^i y ) e. ( (,) " ( S X. S ) ) <-> A. v e. S A. u e. S ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) )
57 45 56 bitrdi 
 |-  ( t = <. z , w >. -> ( A. y e. ( (,) " ( S X. S ) ) ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) <-> A. v e. S A. u e. S ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) ) )
58 57 ralxp 
 |-  ( A. t e. ( S X. S ) A. y e. ( (,) " ( S X. S ) ) ( ( (,) ` t ) i^i y ) e. ( (,) " ( S X. S ) ) <-> A. z e. S A. w e. S A. v e. S A. u e. S ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) )
59 39 58 bitri 
 |-  ( A. x e. ( (,) " ( S X. S ) ) A. y e. ( (,) " ( S X. S ) ) ( x i^i y ) e. ( (,) " ( S X. S ) ) <-> A. z e. S A. w e. S A. v e. S A. u e. S ( ( z (,) w ) i^i ( v (,) u ) ) e. ( (,) " ( S X. S ) ) )
60 32 59 mpbir 
 |-  A. x e. ( (,) " ( S X. S ) ) A. y e. ( (,) " ( S X. S ) ) ( x i^i y ) e. ( (,) " ( S X. S ) )
61 fiinbas 
 |-  ( ( ( (,) " ( S X. S ) ) e. _V /\ A. x e. ( (,) " ( S X. S ) ) A. y e. ( (,) " ( S X. S ) ) ( x i^i y ) e. ( (,) " ( S X. S ) ) ) -> ( (,) " ( S X. S ) ) e. TopBases )
62 3 60 61 mp2an 
 |-  ( (,) " ( S X. S ) ) e. TopBases