This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 ⊆ ℝ*
Assertion qtopbaslem ( (,) “ ( 𝑆 × 𝑆 ) ) ∈ TopBases

Proof

Step Hyp Ref Expression
1 qtopbas.1 ⊢ 𝑆 ⊆ ℝ*
2 iooex ⊢ (,) ∈ V
3 2 imaex ⊢ ( (,) “ ( 𝑆 × 𝑆 ) ) ∈ V
4 1 sseli ⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ℝ* )
5 1 sseli ⊢ ( 𝑤 ∈ 𝑆 → 𝑤 ∈ ℝ* )
6 4 5 anim12i ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) )
7 1 sseli ⊢ ( 𝑣 ∈ 𝑆 → 𝑣 ∈ ℝ* )
8 1 sseli ⊢ ( 𝑢 ∈ 𝑆 → 𝑢 ∈ ℝ* )
9 7 8 anim12i ⊢ ( ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) → ( 𝑣 ∈ ℝ* ∧ 𝑢 ∈ ℝ* ) )
10 iooin ⊢ ( ( ( 𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝑣 ∈ ℝ* ∧ 𝑢 ∈ ℝ* ) ) → ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) = ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) (,) if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ) )
11 6 9 10 syl2an ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) = ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) (,) if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ) )
12 ifcl ⊢ ( ( 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) ∈ 𝑆 )
13 12 ancoms ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) ∈ 𝑆 )
14 ifcl ⊢ ( ( 𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) → if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ∈ 𝑆 )
15 df-ov ⊢ ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) (,) if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ) = ( (,) ‘ ⟨ if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) , if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ⟩ )
16 opelxpi ⊢ ( ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) ∈ 𝑆 ∧ if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ∈ 𝑆 ) → ⟨ if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) , if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ⟩ ∈ ( 𝑆 × 𝑆 ) )
17 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
18 ffun ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → Fun (,) )
19 17 18 ax-mp ⊢ Fun (,)
20 xpss12 ⊢ ( ( 𝑆 ⊆ ℝ* ∧ 𝑆 ⊆ ℝ* ) → ( 𝑆 × 𝑆 ) ⊆ ( ℝ* × ℝ* ) )
21 1 1 20 mp2an ⊢ ( 𝑆 × 𝑆 ) ⊆ ( ℝ* × ℝ* )
22 17 fdmi ⊢ dom (,) = ( ℝ* × ℝ* )
23 21 22 sseqtrri ⊢ ( 𝑆 × 𝑆 ) ⊆ dom (,)
24 funfvima2 ⊢ ( ( Fun (,) ∧ ( 𝑆 × 𝑆 ) ⊆ dom (,) ) → ( ⟨ if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) , if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ⟩ ∈ ( 𝑆 × 𝑆 ) → ( (,) ‘ ⟨ if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) , if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ⟩ ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
25 19 23 24 mp2an ⊢ ( ⟨ if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) , if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ⟩ ∈ ( 𝑆 × 𝑆 ) → ( (,) ‘ ⟨ if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) , if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ⟩ ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
26 16 25 syl ⊢ ( ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) ∈ 𝑆 ∧ if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ∈ 𝑆 ) → ( (,) ‘ ⟨ if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) , if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ⟩ ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
27 15 26 eqeltrid ⊢ ( ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) ∈ 𝑆 ∧ if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ∈ 𝑆 ) → ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) (,) if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
28 13 14 27 syl2an ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) (,) if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
29 28 an4s ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( if ( 𝑧 ≤ 𝑣 , 𝑣 , 𝑧 ) (,) if ( 𝑤 ≤ 𝑢 , 𝑤 , 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
30 11 29 eqeltrd ⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
31 30 ralrimivva ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ∀ 𝑣 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
32 31 rgen2 ⊢ ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) )
33 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
34 17 33 ax-mp ⊢ (,) Fn ( ℝ* × ℝ* )
35 ineq1 ⊢ ( 𝑥 = ( (,) ‘ 𝑡 ) → ( 𝑥 ∩ 𝑦 ) = ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) )
36 35 eleq1d ⊢ ( 𝑥 = ( (,) ‘ 𝑡 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
37 36 ralbidv ⊢ ( 𝑥 = ( (,) ‘ 𝑡 ) → ( ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
38 37 ralima ⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ ( 𝑆 × 𝑆 ) ⊆ ( ℝ* × ℝ* ) ) → ( ∀ 𝑥 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑡 ∈ ( 𝑆 × 𝑆 ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
39 34 21 38 mp2an ⊢ ( ∀ 𝑥 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑡 ∈ ( 𝑆 × 𝑆 ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
40 fveq2 ⊢ ( 𝑡 = ⟨ 𝑧 , 𝑤 ⟩ → ( (,) ‘ 𝑡 ) = ( (,) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
41 df-ov ⊢ ( 𝑧 (,) 𝑤 ) = ( (,) ‘ ⟨ 𝑧 , 𝑤 ⟩ )
42 40 41 eqtr4di ⊢ ( 𝑡 = ⟨ 𝑧 , 𝑤 ⟩ → ( (,) ‘ 𝑡 ) = ( 𝑧 (,) 𝑤 ) )
43 42 ineq1d ⊢ ( 𝑡 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) = ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) )
44 43 eleq1d ⊢ ( 𝑡 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
45 44 ralbidv ⊢ ( 𝑡 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
46 ineq2 ⊢ ( 𝑦 = ( (,) ‘ 𝑡 ) → ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) = ( ( 𝑧 (,) 𝑤 ) ∩ ( (,) ‘ 𝑡 ) ) )
47 46 eleq1d ⊢ ( 𝑦 = ( (,) ‘ 𝑡 ) → ( ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ( ( 𝑧 (,) 𝑤 ) ∩ ( (,) ‘ 𝑡 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
48 47 ralima ⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ ( 𝑆 × 𝑆 ) ⊆ ( ℝ* × ℝ* ) ) → ( ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑡 ∈ ( 𝑆 × 𝑆 ) ( ( 𝑧 (,) 𝑤 ) ∩ ( (,) ‘ 𝑡 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
49 34 21 48 mp2an ⊢ ( ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑡 ∈ ( 𝑆 × 𝑆 ) ( ( 𝑧 (,) 𝑤 ) ∩ ( (,) ‘ 𝑡 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
50 fveq2 ⊢ ( 𝑡 = ⟨ 𝑣 , 𝑢 ⟩ → ( (,) ‘ 𝑡 ) = ( (,) ‘ ⟨ 𝑣 , 𝑢 ⟩ ) )
51 df-ov ⊢ ( 𝑣 (,) 𝑢 ) = ( (,) ‘ ⟨ 𝑣 , 𝑢 ⟩ )
52 50 51 eqtr4di ⊢ ( 𝑡 = ⟨ 𝑣 , 𝑢 ⟩ → ( (,) ‘ 𝑡 ) = ( 𝑣 (,) 𝑢 ) )
53 52 ineq2d ⊢ ( 𝑡 = ⟨ 𝑣 , 𝑢 ⟩ → ( ( 𝑧 (,) 𝑤 ) ∩ ( (,) ‘ 𝑡 ) ) = ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) )
54 53 eleq1d ⊢ ( 𝑡 = ⟨ 𝑣 , 𝑢 ⟩ → ( ( ( 𝑧 (,) 𝑤 ) ∩ ( (,) ‘ 𝑡 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
55 54 ralxp ⊢ ( ∀ 𝑡 ∈ ( 𝑆 × 𝑆 ) ( ( 𝑧 (,) 𝑤 ) ∩ ( (,) ‘ 𝑡 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑣 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
56 49 55 bitri ⊢ ( ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( 𝑧 (,) 𝑤 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑣 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
57 45 56 bitrdi ⊢ ( 𝑡 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑣 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) )
58 57 ralxp ⊢ ( ∀ 𝑡 ∈ ( 𝑆 × 𝑆 ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( ( (,) ‘ 𝑡 ) ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
59 39 58 bitri ⊢ ( ∀ 𝑥 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑧 (,) 𝑤 ) ∩ ( 𝑣 (,) 𝑢 ) ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) )
60 32 59 mpbir ⊢ ∀ 𝑥 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) )
61 fiinbas ⊢ ( ( ( (,) “ ( 𝑆 × 𝑆 ) ) ∈ V ∧ ∀ 𝑥 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ∀ 𝑦 ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( (,) “ ( 𝑆 × 𝑆 ) ) ) → ( (,) “ ( 𝑆 × 𝑆 ) ) ∈ TopBases )
62 3 60 61 mp2an ⊢ ( (,) “ ( 𝑆 × 𝑆 ) ) ∈ TopBases