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