sxbrsigalem3

Description: The sigma-algebra generated by the closed half-spaces of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed sets of ( RR X. RR ) . (Contributed by Thierry Arnoux, 11-Oct-2017)

		Ref	Expression
	Hypothesis	sxbrsiga.0	$⊢ J = topGen (ran (.))$
	Assertion	sxbrsigalem3	$⊢ 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \subseteq 𝛔 (Clsd (J \times_{t} J))$

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	$⊢ J = topGen (ran (.))$
2		sxbrsigalem0	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ℝ^{2}$
3		retop	$⊢ topGen (ran (.)) \in Top$
4	1 3	eqeltri	$⊢ J \in Top$
5	4 4	txtopi	$⊢ J \times_{t} J \in Top$
6		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
7	1	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
8	6 7	eqtr4i	$⊢ ℝ = ⋃ J$
9	4 4 8 8	txunii	$⊢ ℝ^{2} = ⋃ (J \times_{t} J)$
10	5 9	unicls	$⊢ ⋃ Clsd (J \times_{t} J) = ℝ^{2}$
11	2 10	eqtr4i	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ⋃ Clsd (J \times_{t} J)$
12		ovex	$⊢ [e, +∞) \in V$
13		reex	$⊢ ℝ \in V$
14	12 13	xpex	$⊢ [e, +∞) \times ℝ \in V$
15		eqid	$⊢ (e \in ℝ ⟼ [e, +∞) \times ℝ) = (e \in ℝ ⟼ [e, +∞) \times ℝ)$
16	14 15	fnmpti	$⊢ (e \in ℝ ⟼ [e, +∞) \times ℝ) Fn ℝ$
17		oveq1	$⊢ e = u \to [e, +∞) = [u, +∞)$
18	17	xpeq1d	$⊢ e = u \to [e, +∞) \times ℝ = [u, +∞) \times ℝ$
19		ovex	$⊢ [u, +∞) \in V$
20	19 13	xpex	$⊢ [u, +∞) \times ℝ \in V$
21	18 15 20	fvmpt	$⊢ u \in ℝ \to (e \in ℝ ⟼ [e, +∞) \times ℝ) (u) = [u, +∞) \times ℝ$
22		icopnfcld	$⊢ u \in ℝ \to [u, +∞) \in Clsd (topGen (ran (.)))$
23	1	fveq2i	$⊢ Clsd (J) = Clsd (topGen (ran (.)))$
24	22 23	eleqtrrdi	$⊢ u \in ℝ \to [u, +∞) \in Clsd (J)$
25		dif0	$⊢ ℝ ∖ \emptyset = ℝ$
26		0opn	$⊢ J \in Top \to \emptyset \in J$
27	4 26	ax-mp	$⊢ \emptyset \in J$
28	8	opncld	$⊢ (J \in Top \land \emptyset \in J) \to ℝ ∖ \emptyset \in Clsd (J)$
29	4 27 28	mp2an	$⊢ ℝ ∖ \emptyset \in Clsd (J)$
30	25 29	eqeltrri	$⊢ ℝ \in Clsd (J)$
31		txcld	$⊢ ([u, +∞) \in Clsd (J) \land ℝ \in Clsd (J)) \to [u, +∞) \times ℝ \in Clsd (J \times_{t} J)$
32	24 30 31	sylancl	$⊢ u \in ℝ \to [u, +∞) \times ℝ \in Clsd (J \times_{t} J)$
33	21 32	eqeltrd	$⊢ u \in ℝ \to (e \in ℝ ⟼ [e, +∞) \times ℝ) (u) \in Clsd (J \times_{t} J)$
34	33	rgen	$⊢ \forall u \in ℝ (e \in ℝ ⟼ [e, +∞) \times ℝ) (u) \in Clsd (J \times_{t} J)$
35		fnfvrnss	$⊢ ((e \in ℝ ⟼ [e, +∞) \times ℝ) Fn ℝ \land \forall u \in ℝ (e \in ℝ ⟼ [e, +∞) \times ℝ) (u) \in Clsd (J \times_{t} J)) \to ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \subseteq Clsd (J \times_{t} J)$
36	16 34 35	mp2an	$⊢ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \subseteq Clsd (J \times_{t} J)$
37		ovex	$⊢ [f, +∞) \in V$
38	13 37	xpex	$⊢ ℝ \times [f, +∞) \in V$
39		eqid	$⊢ (f \in ℝ ⟼ ℝ \times [f, +∞)) = (f \in ℝ ⟼ ℝ \times [f, +∞))$
40	38 39	fnmpti	$⊢ (f \in ℝ ⟼ ℝ \times [f, +∞)) Fn ℝ$
41		oveq1	$⊢ f = v \to [f, +∞) = [v, +∞)$
42	41	xpeq2d	$⊢ f = v \to ℝ \times [f, +∞) = ℝ \times [v, +∞)$
43		ovex	$⊢ [v, +∞) \in V$
44	13 43	xpex	$⊢ ℝ \times [v, +∞) \in V$
45	42 39 44	fvmpt	$⊢ v \in ℝ \to (f \in ℝ ⟼ ℝ \times [f, +∞)) (v) = ℝ \times [v, +∞)$
46		icopnfcld	$⊢ v \in ℝ \to [v, +∞) \in Clsd (topGen (ran (.)))$
47	46 23	eleqtrrdi	$⊢ v \in ℝ \to [v, +∞) \in Clsd (J)$
48		txcld	$⊢ (ℝ \in Clsd (J) \land [v, +∞) \in Clsd (J)) \to ℝ \times [v, +∞) \in Clsd (J \times_{t} J)$
49	30 47 48	sylancr	$⊢ v \in ℝ \to ℝ \times [v, +∞) \in Clsd (J \times_{t} J)$
50	45 49	eqeltrd	$⊢ v \in ℝ \to (f \in ℝ ⟼ ℝ \times [f, +∞)) (v) \in Clsd (J \times_{t} J)$
51	50	rgen	$⊢ \forall v \in ℝ (f \in ℝ ⟼ ℝ \times [f, +∞)) (v) \in Clsd (J \times_{t} J)$
52		fnfvrnss	$⊢ ((f \in ℝ ⟼ ℝ \times [f, +∞)) Fn ℝ \land \forall v \in ℝ (f \in ℝ ⟼ ℝ \times [f, +∞)) (v) \in Clsd (J \times_{t} J)) \to ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq Clsd (J \times_{t} J)$
53	40 51 52	mp2an	$⊢ ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq Clsd (J \times_{t} J)$
54	36 53	unssi	$⊢ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq Clsd (J \times_{t} J)$
55		fvex	$⊢ Clsd (J \times_{t} J) \in V$
56		sssigagen	$⊢ Clsd (J \times_{t} J) \in V \to Clsd (J \times_{t} J) \subseteq 𝛔 (Clsd (J \times_{t} J))$
57	55 56	ax-mp	$⊢ Clsd (J \times_{t} J) \subseteq 𝛔 (Clsd (J \times_{t} J))$
58	54 57	sstri	$⊢ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq 𝛔 (Clsd (J \times_{t} J))$
59		sigagenss2	$⊢ (⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ⋃ Clsd (J \times_{t} J) \land ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq 𝛔 (Clsd (J \times_{t} J)) \land Clsd (J \times_{t} J) \in V) \to 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \subseteq 𝛔 (Clsd (J \times_{t} J))$
60	11 58 55 59	mp3an	$⊢ 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \subseteq 𝛔 (Clsd (J \times_{t} J))$

Metamath Proof Explorer

Theorem sxbrsigalem3

Proof