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	$⊢ S \subseteq ℝ^{*}$
	Assertion	qtopbaslem	$⊢ (.) [S \times S] \in TopBases$

Proof

Step	Hyp	Ref	Expression
1		qtopbas.1	$⊢ S \subseteq ℝ^{*}$
2		iooex	$⊢ (.) \in V$
3	2	imaex	$⊢ (.) [S \times S] \in V$
4	1	sseli	$⊢ z \in S \to z \in ℝ^{*}$
5	1	sseli	$⊢ w \in S \to w \in ℝ^{*}$
6	4 5	anim12i	$⊢ (z \in S \land w \in S) \to (z \in ℝ^{} \land w \in ℝ^{})$
7	1	sseli	$⊢ v \in S \to v \in ℝ^{*}$
8	1	sseli	$⊢ u \in S \to u \in ℝ^{*}$
9	7 8	anim12i	$⊢ (v \in S \land u \in S) \to (v \in ℝ^{} \land u \in ℝ^{})$
10		iooin	$⊢ ((z \in ℝ^{} \land w \in ℝ^{}) \land (v \in ℝ^{} \land u \in ℝ^{})) \to (z, w) \cap (v, u) = (if (z \leq v, v, z), if (w \leq u, w, u))$
11	6 9 10	syl2an	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to (z, w) \cap (v, u) = (if (z \leq v, v, z), if (w \leq u, w, u))$
12		ifcl	$⊢ (v \in S \land z \in S) \to if (z \leq v, v, z) \in S$
13	12	ancoms	$⊢ (z \in S \land v \in S) \to if (z \leq v, v, z) \in S$
14		ifcl	$⊢ (w \in S \land u \in S) \to if (w \leq u, w, u) \in S$
15		df-ov	$⊢ (if (z \leq v, v, z), if (w \leq u, w, u)) = (.) (⟨if (z \leq v, v, z), if (w \leq u, w, u)⟩)$
16		opelxpi	$⊢ (if (z \leq v, v, z) \in S \land if (w \leq u, w, u) \in S) \to ⟨if (z \leq v, v, z), if (w \leq u, w, u)⟩ \in (S \times S)$
17		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
18		ffun	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to Fun (.)$
19	17 18	ax-mp	$⊢ Fun (.)$
20		xpss12	$⊢ (S \subseteq ℝ^{} \land S \subseteq ℝ^{}) \to S \times S \subseteq ℝ^{} \times ℝ^{}$
21	1 1 20	mp2an	$⊢ S \times S \subseteq ℝ^{} \times ℝ^{}$
22	17	fdmi	$⊢ dom (.) = ℝ^{} \times ℝ^{}$
23	21 22	sseqtrri	$⊢ S \times S \subseteq dom (.)$
24		funfvima2	$⊢ (Fun (.) \land S \times S \subseteq dom (.)) \to (⟨if (z \leq v, v, z), if (w \leq u, w, u)⟩ \in (S \times S) \to (.) (⟨if (z \leq v, v, z), if (w \leq u, w, u)⟩) \in (.) [S \times S])$
25	19 23 24	mp2an	$⊢ ⟨if (z \leq v, v, z), if (w \leq u, w, u)⟩ \in (S \times S) \to (.) (⟨if (z \leq v, v, z), if (w \leq u, w, u)⟩) \in (.) [S \times S]$
26	16 25	syl	$⊢ (if (z \leq v, v, z) \in S \land if (w \leq u, w, u) \in S) \to (.) (⟨if (z \leq v, v, z), if (w \leq u, w, u)⟩) \in (.) [S \times S]$
27	15 26	eqeltrid	$⊢ (if (z \leq v, v, z) \in S \land if (w \leq u, w, u) \in S) \to (if (z \leq v, v, z), if (w \leq u, w, u)) \in (.) [S \times S]$
28	13 14 27	syl2an	$⊢ ((z \in S \land v \in S) \land (w \in S \land u \in S)) \to (if (z \leq v, v, z), if (w \leq u, w, u)) \in (.) [S \times S]$
29	28	an4s	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to (if (z \leq v, v, z), if (w \leq u, w, u)) \in (.) [S \times S]$
30	11 29	eqeltrd	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to (z, w) \cap (v, u) \in (.) [S \times S]$
31	30	ralrimivva	$⊢ (z \in S \land w \in S) \to \forall v \in S \forall u \in S (z, w) \cap (v, u) \in (.) [S \times S]$
32	31	rgen2	$⊢ \forall z \in S \forall w \in S \forall v \in S \forall u \in S (z, w) \cap (v, u) \in (.) [S \times S]$
33		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
34	17 33	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
35		ineq1	$⊢ x = (.) (t) \to x \cap y = (.) (t) \cap y$
36	35	eleq1d	$⊢ x = (.) (t) \to (x \cap y \in (.) [S \times S] \leftrightarrow (.) (t) \cap y \in (.) [S \times S])$
37	36	ralbidv	$⊢ x = (.) (t) \to (\forall y \in (.) [S \times S] x \cap y \in (.) [S \times S] \leftrightarrow \forall y \in (.) [S \times S] (.) (t) \cap y \in (.) [S \times S])$
38	37	ralima	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land S \times S \subseteq ℝ^{} \times ℝ^{}) \to (\forall x \in (.) [S \times S] \forall y \in (.) [S \times S] x \cap y \in (.) [S \times S] \leftrightarrow \forall t \in (S \times S) \forall y \in (.) [S \times S] (.) (t) \cap y \in (.) [S \times S])$
39	34 21 38	mp2an	$⊢ \forall x \in (.) [S \times S] \forall y \in (.) [S \times S] x \cap y \in (.) [S \times S] \leftrightarrow \forall t \in (S \times S) \forall y \in (.) [S \times S] (.) (t) \cap y \in (.) [S \times S]$
40		fveq2	$⊢ t = ⟨z, w⟩ \to (.) (t) = (.) (⟨z, w⟩)$
41		df-ov	$⊢ (z, w) = (.) (⟨z, w⟩)$
42	40 41	syl6eqr	$⊢ t = ⟨z, w⟩ \to (.) (t) = (z, w)$
43	42	ineq1d	$⊢ t = ⟨z, w⟩ \to (.) (t) \cap y = (z, w) \cap y$
44	43	eleq1d	$⊢ t = ⟨z, w⟩ \to ((.) (t) \cap y \in (.) [S \times S] \leftrightarrow (z, w) \cap y \in (.) [S \times S])$
45	44	ralbidv	$⊢ t = ⟨z, w⟩ \to (\forall y \in (.) [S \times S] (.) (t) \cap y \in (.) [S \times S] \leftrightarrow \forall y \in (.) [S \times S] (z, w) \cap y \in (.) [S \times S])$
46		ineq2	$⊢ y = (.) (t) \to (z, w) \cap y = (z, w) \cap (.) (t)$
47	46	eleq1d	$⊢ y = (.) (t) \to ((z, w) \cap y \in (.) [S \times S] \leftrightarrow (z, w) \cap (.) (t) \in (.) [S \times S])$
48	47	ralima	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land S \times S \subseteq ℝ^{} \times ℝ^{}) \to (\forall y \in (.) [S \times S] (z, w) \cap y \in (.) [S \times S] \leftrightarrow \forall t \in (S \times S) (z, w) \cap (.) (t) \in (.) [S \times S])$
49	34 21 48	mp2an	$⊢ \forall y \in (.) [S \times S] (z, w) \cap y \in (.) [S \times S] \leftrightarrow \forall t \in (S \times S) (z, w) \cap (.) (t) \in (.) [S \times S]$
50		fveq2	$⊢ t = ⟨v, u⟩ \to (.) (t) = (.) (⟨v, u⟩)$
51		df-ov	$⊢ (v, u) = (.) (⟨v, u⟩)$
52	50 51	syl6eqr	$⊢ t = ⟨v, u⟩ \to (.) (t) = (v, u)$
53	52	ineq2d	$⊢ t = ⟨v, u⟩ \to (z, w) \cap (.) (t) = (z, w) \cap (v, u)$
54	53	eleq1d	$⊢ t = ⟨v, u⟩ \to ((z, w) \cap (.) (t) \in (.) [S \times S] \leftrightarrow (z, w) \cap (v, u) \in (.) [S \times S])$
55	54	ralxp	$⊢ \forall t \in (S \times S) (z, w) \cap (.) (t) \in (.) [S \times S] \leftrightarrow \forall v \in S \forall u \in S (z, w) \cap (v, u) \in (.) [S \times S]$
56	49 55	bitri	$⊢ \forall y \in (.) [S \times S] (z, w) \cap y \in (.) [S \times S] \leftrightarrow \forall v \in S \forall u \in S (z, w) \cap (v, u) \in (.) [S \times S]$
57	45 56	syl6bb	$⊢ t = ⟨z, w⟩ \to (\forall y \in (.) [S \times S] (.) (t) \cap y \in (.) [S \times S] \leftrightarrow \forall v \in S \forall u \in S (z, w) \cap (v, u) \in (.) [S \times S])$
58	57	ralxp	$⊢ \forall t \in (S \times S) \forall y \in (.) [S \times S] (.) (t) \cap y \in (.) [S \times S] \leftrightarrow \forall z \in S \forall w \in S \forall v \in S \forall u \in S (z, w) \cap (v, u) \in (.) [S \times S]$
59	39 58	bitri	$⊢ \forall x \in (.) [S \times S] \forall y \in (.) [S \times S] x \cap y \in (.) [S \times S] \leftrightarrow \forall z \in S \forall w \in S \forall v \in S \forall u \in S (z, w) \cap (v, u) \in (.) [S \times S]$
60	32 59	mpbir	$⊢ \forall x \in (.) [S \times S] \forall y \in (.) [S \times S] x \cap y \in (.) [S \times S]$
61		fiinbas	$⊢ ((.) [S \times S] \in V \land \forall x \in (.) [S \times S] \forall y \in (.) [S \times S] x \cap y \in (.) [S \times S]) \to (.) [S \times S] \in TopBases$
62	3 60 61	mp2an	$⊢ (.) [S \times S] \in TopBases$

Metamath Proof Explorer

Theorem qtopbaslem

Proof