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 23628

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 12941	. . 3 ⊢ (,) ∈ V
2	1	imaex 7683	. 2 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ V
3		qtopbas.1	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ^*
4	3	sseli 3887	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ℝ^*)
5	3	sseli 3887	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑆 → 𝑤 ∈ ℝ^*)
6	4, 5	anim12i 616	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*))
7	3	sseli 3887	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ ℝ^*)
8	3	sseli 3887	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℝ^*)
9	7, 8	anim12i 616	. . . . . . 7 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑣 ∈ ℝ^* ∧ 𝑢 ∈ ℝ^*))
10		iooin 12952	. . . . . . 7 ⊢ (((𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑢 ∈ ℝ^*)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
11	6, 9, 10	syl2an 599	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
12		ifcl 4474	. . . . . . . . 9 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
13	12	ancoms 462	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
14		ifcl 4474	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆)
15		df-ov 7205	. . . . . . . . 9 ⊢ (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) = ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩)
16		opelxpi 5577	. . . . . . . . . 10 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆))
17		ioof 13018	. . . . . . . . . . . 12 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffun 6537	. . . . . . . . . . . 12 ⊢ ((,):(ℝ^* × ℝ^*)⟶𝒫 ℝ → Fun (,))
19	17, 18	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (,)
20		xpss12 5555	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ ℝ^* ∧ 𝑆 ⊆ ℝ^) → (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*))
21	3, 3, 20	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑆 × 𝑆) ⊆ (ℝ^* × ℝ^*)
22	17	fdmi 6546	. . . . . . . . . . . 12 ⊢ dom (,) = (ℝ^* × ℝ^*)
23	21, 22	sseqtrri 3928	. . . . . . . . . . 11 ⊢ (𝑆 × 𝑆) ⊆ dom (,)
24		funfvima2 7036	. . . . . . . . . . 11 ⊢ ((Fun (,) ∧ (𝑆 × 𝑆) ⊆ dom (,)) → (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆))))
25	19, 23, 24	mp2an 692	. . . . . . . . . 10 ⊢ (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
26	16, 25	syl 17	. . . . . . . . 9 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
27	15, 26	eqeltrid 2838	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
28	13, 14, 27	syl2an 599	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
29	28	an4s 660	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
30	11, 29	eqeltrd 2834	. . . . 5 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
31	30	ralrimivva 3105	. . . 4 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
32	31	rgen2 3117	. . 3 ⊢ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))
33		ffn 6534	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
34	17, 33	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
35		ineq1 4110	. . . . . . . 8 ⊢ (𝑥 = ((,)‘𝑡) → (𝑥 ∩ 𝑦) = (((,)‘𝑡) ∩ 𝑦))
36	35	eleq1d 2818	. . . . . . 7 ⊢ (𝑥 = ((,)‘𝑡) → ((𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ (((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
37	36	ralbidv 3111	. . . . . 6 ⊢ (𝑥 = ((,)‘𝑡) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
38	37	ralima 7043	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
39	34, 21, 38	mp2an 692	. . . 4 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))
40		fveq2 6706	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = ((,)‘⟨𝑧, 𝑤⟩))
41		df-ov 7205	. . . . . . . . . 10 ⊢ (𝑧(,)𝑤) = ((,)‘⟨𝑧, 𝑤⟩)
42	40, 41	eqtr4di 2792	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = (𝑧(,)𝑤))
43	42	ineq1d 4116	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (((,)‘𝑡) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ 𝑦))
44	43	eleq1d 2818	. . . . . . 7 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
45	44	ralbidv 3111	. . . . . 6 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
46		ineq2 4111	. . . . . . . . . 10 ⊢ (𝑦 = ((,)‘𝑡) → ((𝑧(,)𝑤) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ ((,)‘𝑡)))
47	46	eleq1d 2818	. . . . . . . . 9 ⊢ (𝑦 = ((,)‘𝑡) → (((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
48	47	ralima 7043	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
49	34, 21, 48	mp2an 692	. . . . . . 7 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)))
50		fveq2 6706	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = ((,)‘⟨𝑣, 𝑢⟩))
51		df-ov 7205	. . . . . . . . . . 11 ⊢ (𝑣(,)𝑢) = ((,)‘⟨𝑣, 𝑢⟩)
52	50, 51	eqtr4di 2792	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = (𝑣(,)𝑢))
53	52	ineq2d 4117	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) = ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)))
54	53	eleq1d 2818	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → (((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
55	54	ralxp 5699	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
56	49, 55	bitri 278	. . . . . 6 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
57	45, 56	bitrdi 290	. . . . 5 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
58	57	ralxp 5699	. . . 4 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
59	39, 58	bitri 278	. . 3 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
60	32, 59	mpbir 234	. 2 ⊢ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))
61		fiinbas 21821	. 2 ⊢ ((((,) “ (𝑆 × 𝑆)) ∈ V ∧ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))) → ((,) “ (𝑆 × 𝑆)) ∈ TopBases)
62	2, 60, 61	mp2an 692	1 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ∀wral 3054 Vcvv 3401 ∩ cin 3856 ⊆ wss 3857 ifcif 4429 𝒫 cpw 4503 ⟨cop 4537 class class class wbr 5043 × cxp 5538 dom cdm 5540 “ cima 5543 Fun wfun 6363 Fn wfn 6364 ⟶wf 6365 ‘cfv 6369 (class class class)co 7202 ℝcr 10711 ℝ^*cxr 10849 ≤ cle 10851 (,)cioo 12918 TopBasesctb 21814

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-pre-lttri 10786 ax-pre-lttrn 10787

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-op 4538 df-uni 4810 df-iun 4896 df-br 5044 df-opab 5106 df-mpt 5125 df-id 5444 df-po 5457 df-so 5458 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-ov 7205 df-oprab 7206 df-mpo 7207 df-1st 7750 df-2nd 7751 df-er 8380 df-en 8616 df-dom 8617 df-sdom 8618 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-ioo 12922 df-bases 21815

This theorem is referenced by: qtopbas 23629 retopbas 23630

W3C validator