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 23828

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 13031	. . 3 ⊢ (,) ∈ V
2	1	imaex 7737	. 2 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ V
3		qtopbas.1	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ^*
4	3	sseli 3913	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ℝ^*)
5	3	sseli 3913	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑆 → 𝑤 ∈ ℝ^*)
6	4, 5	anim12i 612	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*))
7	3	sseli 3913	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ ℝ^*)
8	3	sseli 3913	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℝ^*)
9	7, 8	anim12i 612	. . . . . . 7 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑣 ∈ ℝ^* ∧ 𝑢 ∈ ℝ^*))
10		iooin 13042	. . . . . . 7 ⊢ (((𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑢 ∈ ℝ^*)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
11	6, 9, 10	syl2an 595	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
12		ifcl 4501	. . . . . . . . 9 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
13	12	ancoms 458	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
14		ifcl 4501	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆)
15		df-ov 7258	. . . . . . . . 9 ⊢ (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) = ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩)
16		opelxpi 5617	. . . . . . . . . 10 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆))
17		ioof 13108	. . . . . . . . . . . 12 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffun 6587	. . . . . . . . . . . 12 ⊢ ((,):(ℝ^* × ℝ^*)⟶𝒫 ℝ → Fun (,))
19	17, 18	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (,)
20		xpss12 5595	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ ℝ^* ∧ 𝑆 ⊆ ℝ^) → (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*))
21	3, 3, 20	mp2an 688	. . . . . . . . . . . 12 ⊢ (𝑆 × 𝑆) ⊆ (ℝ^* × ℝ^*)
22	17	fdmi 6596	. . . . . . . . . . . 12 ⊢ dom (,) = (ℝ^* × ℝ^*)
23	21, 22	sseqtrri 3954	. . . . . . . . . . 11 ⊢ (𝑆 × 𝑆) ⊆ dom (,)
24		funfvima2 7089	. . . . . . . . . . 11 ⊢ ((Fun (,) ∧ (𝑆 × 𝑆) ⊆ dom (,)) → (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆))))
25	19, 23, 24	mp2an 688	. . . . . . . . . 10 ⊢ (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
26	16, 25	syl 17	. . . . . . . . 9 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
27	15, 26	eqeltrid 2843	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
28	13, 14, 27	syl2an 595	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
29	28	an4s 656	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
30	11, 29	eqeltrd 2839	. . . . 5 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
31	30	ralrimivva 3114	. . . 4 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
32	31	rgen2 3126	. . 3 ⊢ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))
33		ffn 6584	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
34	17, 33	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
35		ineq1 4136	. . . . . . . 8 ⊢ (𝑥 = ((,)‘𝑡) → (𝑥 ∩ 𝑦) = (((,)‘𝑡) ∩ 𝑦))
36	35	eleq1d 2823	. . . . . . 7 ⊢ (𝑥 = ((,)‘𝑡) → ((𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ (((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
37	36	ralbidv 3120	. . . . . 6 ⊢ (𝑥 = ((,)‘𝑡) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
38	37	ralima 7096	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
39	34, 21, 38	mp2an 688	. . . 4 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))
40		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = ((,)‘⟨𝑧, 𝑤⟩))
41		df-ov 7258	. . . . . . . . . 10 ⊢ (𝑧(,)𝑤) = ((,)‘⟨𝑧, 𝑤⟩)
42	40, 41	eqtr4di 2797	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = (𝑧(,)𝑤))
43	42	ineq1d 4142	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (((,)‘𝑡) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ 𝑦))
44	43	eleq1d 2823	. . . . . . 7 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
45	44	ralbidv 3120	. . . . . 6 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
46		ineq2 4137	. . . . . . . . . 10 ⊢ (𝑦 = ((,)‘𝑡) → ((𝑧(,)𝑤) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ ((,)‘𝑡)))
47	46	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑦 = ((,)‘𝑡) → (((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
48	47	ralima 7096	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
49	34, 21, 48	mp2an 688	. . . . . . 7 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)))
50		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = ((,)‘⟨𝑣, 𝑢⟩))
51		df-ov 7258	. . . . . . . . . . 11 ⊢ (𝑣(,)𝑢) = ((,)‘⟨𝑣, 𝑢⟩)
52	50, 51	eqtr4di 2797	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = (𝑣(,)𝑢))
53	52	ineq2d 4143	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) = ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)))
54	53	eleq1d 2823	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → (((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
55	54	ralxp 5739	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
56	49, 55	bitri 274	. . . . . 6 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
57	45, 56	bitrdi 286	. . . . 5 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
58	57	ralxp 5739	. . . 4 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
59	39, 58	bitri 274	. . 3 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
60	32, 59	mpbir 230	. 2 ⊢ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))
61		fiinbas 22010	. 2 ⊢ ((((,) “ (𝑆 × 𝑆)) ∈ V ∧ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))) → ((,) “ (𝑆 × 𝑆)) ∈ TopBases)
62	2, 60, 61	mp2an 688	1 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∀wral 3063 Vcvv 3422 ∩ cin 3882 ⊆ wss 3883 ifcif 4456 𝒫 cpw 4530 ⟨cop 4564 class class class wbr 5070 × cxp 5578 dom cdm 5580 “ cima 5583 Fun wfun 6412 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ℝcr 10801 ℝ^*cxr 10939 ≤ cle 10941 (,)cioo 13008 TopBasesctb 22003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-pre-lttri 10876 ax-pre-lttrn 10877

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-po 5494 df-so 5495 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-oprab 7259 df-mpo 7260 df-1st 7804 df-2nd 7805 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-ioo 13012 df-bases 22004

This theorem is referenced by: qtopbas 23829 retopbas 23830

W3C validator