qtopbaslem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > qtopbaslem		Structured version Visualization version GIF version

Theorem qtopbaslem 23367

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

**Hypothesis**
Ref	Expression
qtopbas.1	⊢ 𝑆 ⊆ ℝ^*

**Assertion**
Ref	Expression
qtopbaslem	⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases

Proof of Theorem qtopbaslem Dummy variables 𝑢 𝑡 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iooex 12762	. . 3 ⊢ (,) ∈ V
2	1	imaex 7621	. 2 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ V
3		qtopbas.1	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ^*
4	3	sseli 3963	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ℝ^*)
5	3	sseli 3963	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑆 → 𝑤 ∈ ℝ^*)
6	4, 5	anim12i 614	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*))
7	3	sseli 3963	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ ℝ^*)
8	3	sseli 3963	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℝ^*)
9	7, 8	anim12i 614	. . . . . . 7 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑣 ∈ ℝ^* ∧ 𝑢 ∈ ℝ^*))
10		iooin 12773	. . . . . . 7 ⊢ (((𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑢 ∈ ℝ^*)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
11	6, 9, 10	syl2an 597	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
12		ifcl 4511	. . . . . . . . 9 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
13	12	ancoms 461	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
14		ifcl 4511	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆)
15		df-ov 7159	. . . . . . . . 9 ⊢ (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) = ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩)
16		opelxpi 5592	. . . . . . . . . 10 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆))
17		ioof 12836	. . . . . . . . . . . 12 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffun 6517	. . . . . . . . . . . 12 ⊢ ((,):(ℝ^* × ℝ^*)⟶𝒫 ℝ → Fun (,))
19	17, 18	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (,)
20		xpss12 5570	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ ℝ^* ∧ 𝑆 ⊆ ℝ^) → (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*))
21	3, 3, 20	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝑆 × 𝑆) ⊆ (ℝ^* × ℝ^*)
22	17	fdmi 6524	. . . . . . . . . . . 12 ⊢ dom (,) = (ℝ^* × ℝ^*)
23	21, 22	sseqtrri 4004	. . . . . . . . . . 11 ⊢ (𝑆 × 𝑆) ⊆ dom (,)
24		funfvima2 6993	. . . . . . . . . . 11 ⊢ ((Fun (,) ∧ (𝑆 × 𝑆) ⊆ dom (,)) → (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆))))
25	19, 23, 24	mp2an 690	. . . . . . . . . 10 ⊢ (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
26	16, 25	syl 17	. . . . . . . . 9 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
27	15, 26	eqeltrid 2917	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
28	13, 14, 27	syl2an 597	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
29	28	an4s 658	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
30	11, 29	eqeltrd 2913	. . . . 5 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
31	30	ralrimivva 3191	. . . 4 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
32	31	rgen2 3203	. . 3 ⊢ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))
33		ffn 6514	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
34	17, 33	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
35		ineq1 4181	. . . . . . . 8 ⊢ (𝑥 = ((,)‘𝑡) → (𝑥 ∩ 𝑦) = (((,)‘𝑡) ∩ 𝑦))
36	35	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = ((,)‘𝑡) → ((𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ (((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
37	36	ralbidv 3197	. . . . . 6 ⊢ (𝑥 = ((,)‘𝑡) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
38	37	ralima 7000	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
39	34, 21, 38	mp2an 690	. . . 4 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))
40		fveq2 6670	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = ((,)‘⟨𝑧, 𝑤⟩))
41		df-ov 7159	. . . . . . . . . 10 ⊢ (𝑧(,)𝑤) = ((,)‘⟨𝑧, 𝑤⟩)
42	40, 41	syl6eqr 2874	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = (𝑧(,)𝑤))
43	42	ineq1d 4188	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (((,)‘𝑡) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ 𝑦))
44	43	eleq1d 2897	. . . . . . 7 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
45	44	ralbidv 3197	. . . . . 6 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
46		ineq2 4183	. . . . . . . . . 10 ⊢ (𝑦 = ((,)‘𝑡) → ((𝑧(,)𝑤) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ ((,)‘𝑡)))
47	46	eleq1d 2897	. . . . . . . . 9 ⊢ (𝑦 = ((,)‘𝑡) → (((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
48	47	ralima 7000	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
49	34, 21, 48	mp2an 690	. . . . . . 7 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)))
50		fveq2 6670	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = ((,)‘⟨𝑣, 𝑢⟩))
51		df-ov 7159	. . . . . . . . . . 11 ⊢ (𝑣(,)𝑢) = ((,)‘⟨𝑣, 𝑢⟩)
52	50, 51	syl6eqr 2874	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = (𝑣(,)𝑢))
53	52	ineq2d 4189	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) = ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)))
54	53	eleq1d 2897	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → (((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
55	54	ralxp 5712	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
56	49, 55	bitri 277	. . . . . 6 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
57	45, 56	syl6bb 289	. . . . 5 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
58	57	ralxp 5712	. . . 4 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
59	39, 58	bitri 277	. . 3 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
60	32, 59	mpbir 233	. 2 ⊢ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))
61		fiinbas 21560	. 2 ⊢ ((((,) “ (𝑆 × 𝑆)) ∈ V ∧ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))) → ((,) “ (𝑆 × 𝑆)) ∈ TopBases)
62	2, 60, 61	mp2an 690	1 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ∀wral 3138 Vcvv 3494 ∩ cin 3935 ⊆ wss 3936 ifcif 4467 𝒫 cpw 4539 ⟨cop 4573 class class class wbr 5066 × cxp 5553 dom cdm 5555 “ cima 5558 Fun wfun 6349 Fn wfn 6350 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 ℝcr 10536 ℝ^*cxr 10674 ≤ cle 10676 (,)cioo 12739 TopBasesctb 21553

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-pre-lttri 10611 ax-pre-lttrn 10612

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-po 5474 df-so 5475 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-ov 7159 df-oprab 7160 df-mpo 7161 df-1st 7689 df-2nd 7690 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-ioo 12743 df-bases 21554

This theorem is referenced by: qtopbas 23368 retopbas 23369

W3C validator