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 24597

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 13344	. . 3 ⊢ (,) ∈ V
2	1	imaex 7900	. 2 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ V
3		qtopbas.1	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ^*
4	3	sseli 3970	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ℝ^*)
5	3	sseli 3970	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑆 → 𝑤 ∈ ℝ^*)
6	4, 5	anim12i 612	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*))
7	3	sseli 3970	. . . . . . . 8 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ ℝ^*)
8	3	sseli 3970	. . . . . . . 8 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℝ^*)
9	7, 8	anim12i 612	. . . . . . 7 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑣 ∈ ℝ^* ∧ 𝑢 ∈ ℝ^*))
10		iooin 13355	. . . . . . 7 ⊢ (((𝑧 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑣 ∈ ℝ^ ∧ 𝑢 ∈ ℝ^*)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
11	6, 9, 10	syl2an 595	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)))
12		ifcl 4565	. . . . . . . . 9 ⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
13	12	ancoms 458	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆)
14		ifcl 4565	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆)
15		df-ov 7404	. . . . . . . . 9 ⊢ (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) = ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩)
16		opelxpi 5703	. . . . . . . . . 10 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆))
17		ioof 13421	. . . . . . . . . . . 12 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffun 6710	. . . . . . . . . . . 12 ⊢ ((,):(ℝ^* × ℝ^*)⟶𝒫 ℝ → Fun (,))
19	17, 18	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (,)
20		xpss12 5681	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ ℝ^* ∧ 𝑆 ⊆ ℝ^) → (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*))
21	3, 3, 20	mp2an 689	. . . . . . . . . . . 12 ⊢ (𝑆 × 𝑆) ⊆ (ℝ^* × ℝ^*)
22	17	fdmi 6719	. . . . . . . . . . . 12 ⊢ dom (,) = (ℝ^* × ℝ^*)
23	21, 22	sseqtrri 4011	. . . . . . . . . . 11 ⊢ (𝑆 × 𝑆) ⊆ dom (,)
24		funfvima2 7224	. . . . . . . . . . 11 ⊢ ((Fun (,) ∧ (𝑆 × 𝑆) ⊆ dom (,)) → (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆))))
25	19, 23, 24	mp2an 689	. . . . . . . . . 10 ⊢ (⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩ ∈ (𝑆 × 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
26	16, 25	syl 17	. . . . . . . . 9 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ((,)‘⟨if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)⟩) ∈ ((,) “ (𝑆 × 𝑆)))
27	15, 26	eqeltrid 2829	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
28	13, 14, 27	syl2an 595	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
29	28	an4s 657	. . . . . 6 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
30	11, 29	eqeltrd 2825	. . . . 5 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
31	30	ralrimivva 3192	. . . 4 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
32	31	rgen2 3189	. . 3 ⊢ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))
33		ffn 6707	. . . . . 6 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
34	17, 33	ax-mp 5	. . . . 5 ⊢ (,) Fn (ℝ^* × ℝ^*)
35		ineq1 4197	. . . . . . . 8 ⊢ (𝑥 = ((,)‘𝑡) → (𝑥 ∩ 𝑦) = (((,)‘𝑡) ∩ 𝑦))
36	35	eleq1d 2810	. . . . . . 7 ⊢ (𝑥 = ((,)‘𝑡) → ((𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ (((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
37	36	ralbidv 3169	. . . . . 6 ⊢ (𝑥 = ((,)‘𝑡) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
38	37	ralima 7231	. . . . 5 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
39	34, 21, 38	mp2an 689	. . . 4 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))
40		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = ((,)‘⟨𝑧, 𝑤⟩))
41		df-ov 7404	. . . . . . . . . 10 ⊢ (𝑧(,)𝑤) = ((,)‘⟨𝑧, 𝑤⟩)
42	40, 41	eqtr4di 2782	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((,)‘𝑡) = (𝑧(,)𝑤))
43	42	ineq1d 4203	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (((,)‘𝑡) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ 𝑦))
44	43	eleq1d 2810	. . . . . . 7 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → ((((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
45	44	ralbidv 3169	. . . . . 6 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))))
46		ineq2 4198	. . . . . . . . . 10 ⊢ (𝑦 = ((,)‘𝑡) → ((𝑧(,)𝑤) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ ((,)‘𝑡)))
47	46	eleq1d 2810	. . . . . . . . 9 ⊢ (𝑦 = ((,)‘𝑡) → (((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
48	47	ralima 7231	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑆 × 𝑆) ⊆ (ℝ^ × ℝ^*)) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))))
49	34, 21, 48	mp2an 689	. . . . . . 7 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)))
50		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = ((,)‘⟨𝑣, 𝑢⟩))
51		df-ov 7404	. . . . . . . . . . 11 ⊢ (𝑣(,)𝑢) = ((,)‘⟨𝑣, 𝑢⟩)
52	50, 51	eqtr4di 2782	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((,)‘𝑡) = (𝑣(,)𝑢))
53	52	ineq2d 4204	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) = ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)))
54	53	eleq1d 2810	. . . . . . . 8 ⊢ (𝑡 = ⟨𝑣, 𝑢⟩ → (((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
55	54	ralxp 5831	. . . . . . 7 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
56	49, 55	bitri 275	. . . . . 6 ⊢ (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
57	45, 56	bitrdi 287	. . . . 5 ⊢ (𝑡 = ⟨𝑧, 𝑤⟩ → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))))
58	57	ralxp 5831	. . . 4 ⊢ (∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
59	39, 58	bitri 275	. . 3 ⊢ (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))
60	32, 59	mpbir 230	. 2 ⊢ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))
61		fiinbas 22777	. 2 ⊢ ((((,) “ (𝑆 × 𝑆)) ∈ V ∧ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))) → ((,) “ (𝑆 × 𝑆)) ∈ TopBases)
62	2, 60, 61	mp2an 689	1 ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ∀wral 3053 Vcvv 3466 ∩ cin 3939 ⊆ wss 3940 ifcif 4520 𝒫 cpw 4594 ⟨cop 4626 class class class wbr 5138 × cxp 5664 dom cdm 5666 “ cima 5669 Fun wfun 6527 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7401 ℝcr 11105 ℝ^*cxr 11244 ≤ cle 11246 (,)cioo 13321 TopBasesctb 22770

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 ax-pre-lttri 11180 ax-pre-lttrn 11181

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-po 5578 df-so 5579 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7404 df-oprab 7405 df-mpo 7406 df-1st 7968 df-2nd 7969 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-ioo 13325 df-bases 22771

This theorem is referenced by: qtopbas 24598 retopbas 24599

W3C validator