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 *
Assertion qtopbaslem . S × S TopBases

Proof

Step Hyp Ref Expression
1 qtopbas.1 S *
2 iooex . V
3 2 imaex . S × S V
4 1 sseli z S z *
5 1 sseli w S w *
6 4 5 anim12i z S w S z * w *
7 1 sseli v S v *
8 1 sseli u S u *
9 7 8 anim12i v S u S v * u *
10 iooin z * w * v * u * z w v u = if z v v z if w u w u
11 6 9 10 syl2an z S w S v S u S z w v u = if z v v z if w u w u
12 ifcl v S z S if z v v z S
13 12 ancoms z S v S if z v v z S
14 ifcl w S u S if w u w u 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 S if w u w u S if z v v z if w u w u S × S
17 ioof . : * × * 𝒫
18 ffun . : * × * 𝒫 Fun .
19 17 18 ax-mp Fun .
20 xpss12 S * S * S × S * × *
21 1 1 20 mp2an S × S * × *
22 17 fdmi dom . = * × *
23 21 22 sseqtrri S × S dom .
24 funfvima2 Fun . S × S dom . if z v v z if w u w u S × S . if z v v z if w u w u . S × S
25 19 23 24 mp2an if z v v z if w u w u S × S . if z v v z if w u w u . S × S
26 16 25 syl if z v v z S if w u w u S . if z v v z if w u w u . S × S
27 15 26 eqeltrid if z v v z S if w u w u S if z v v z if w u w u . S × S
28 13 14 27 syl2an z S v S w S u S if z v v z if w u w u . S × S
29 28 an4s z S w S v S u S if z v v z if w u w u . S × S
30 11 29 eqeltrd z S w S v S u S z w v u . S × S
31 30 ralrimivva z S w S v S u S z w v u . S × S
32 31 rgen2 z S w S v S u S z w v u . S × S
33 ffn . : * × * 𝒫 . Fn * × *
34 17 33 ax-mp . Fn * × *
35 ineq1 x = . t x y = . t y
36 35 eleq1d x = . t x y . S × S . t y . S × S
37 36 ralbidv x = . t y . S × S x y . S × S y . S × S . t y . S × S
38 37 ralima . Fn * × * S × S * × * x . S × S y . S × S x y . S × S t S × S y . S × S . t y . S × S
39 34 21 38 mp2an x . S × S y . S × S x y . S × S t S × S y . S × S . t y . S × 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 y = z w y
44 43 eleq1d t = z w . t y . S × S z w y . S × S
45 44 ralbidv t = z w y . S × S . t y . S × S y . S × S z w y . S × S
46 ineq2 y = . t z w y = z w . t
47 46 eleq1d y = . t z w y . S × S z w . t . S × S
48 47 ralima . Fn * × * S × S * × * y . S × S z w y . S × S t S × S z w . t . S × S
49 34 21 48 mp2an y . S × S z w y . S × S t S × S z w . t . S × 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 . t = z w v u
54 53 eleq1d t = v u z w . t . S × S z w v u . S × S
55 54 ralxp t S × S z w . t . S × S v S u S z w v u . S × S
56 49 55 bitri y . S × S z w y . S × S v S u S z w v u . S × S
57 45 56 bitrdi t = z w y . S × S . t y . S × S v S u S z w v u . S × S
58 57 ralxp t S × S y . S × S . t y . S × S z S w S v S u S z w v u . S × S
59 39 58 bitri x . S × S y . S × S x y . S × S z S w S v S u S z w v u . S × S
60 32 59 mpbir x . S × S y . S × S x y . S × S
61 fiinbas . S × S V x . S × S y . S × S x y . S × S . S × S TopBases
62 3 60 61 mp2an . S × S TopBases