Theorem 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	⊢ 𝐽 = ( topGen ‘ ran (,) )
Assertion	sxbrsigalem3	⊢ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		sxbrsigalem0	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ )
3		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
4	1 3	eqeltri	⊢ 𝐽 ∈ Top
5	4 4	txtopi	⊢ ( 𝐽 ×t 𝐽 ) ∈ Top
6		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
7	1	unieqi	⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
8	6 7	eqtr4i	⊢ ℝ = ∪ 𝐽
9	4 4 8 8	txunii	⊢ ( ℝ × ℝ ) = ∪ ( 𝐽 ×t 𝐽 )
10	5 9	unicls	⊢ ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) = ( ℝ × ℝ )
11	2 10	eqtr4i	⊢ ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
12		ovex	⊢ ( 𝑒 [,) +∞ ) ∈ V
13		reex	⊢ ℝ ∈ V
14	12 13	xpex	⊢ ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ V
15		eqid	⊢ ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) = ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) )
16	14 15	fnmpti	⊢ ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) Fn ℝ
17		oveq1	⊢ ( 𝑒 = 𝑢 → ( 𝑒 [,) +∞ ) = ( 𝑢 [,) +∞ ) )
18	17	xpeq1d	⊢ ( 𝑒 = 𝑢 → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( 𝑢 [,) +∞ ) × ℝ ) )
19		ovex	⊢ ( 𝑢 [,) +∞ ) ∈ V
20	19 13	xpex	⊢ ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ V
21	18 15 20	fvmpt	⊢ ( 𝑢 ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) = ( ( 𝑢 [,) +∞ ) × ℝ ) )
22		icopnfcld	⊢ ( 𝑢 ∈ ℝ → ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
23	1	fveq2i	⊢ ( Clsd ‘ 𝐽 ) = ( Clsd ‘ ( topGen ‘ ran (,) ) )
24	22 23	eleqtrrdi	⊢ ( 𝑢 ∈ ℝ → ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) )
25		dif0	⊢ ( ℝ ∖ ∅ ) = ℝ
26		0opn	⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
27	4 26	ax-mp	⊢ ∅ ∈ 𝐽
28	8	opncld	⊢ ( ( 𝐽 ∈ Top ∧ ∅ ∈ 𝐽 ) → ( ℝ ∖ ∅ ) ∈ ( Clsd ‘ 𝐽 ) )
29	4 27 28	mp2an	⊢ ( ℝ ∖ ∅ ) ∈ ( Clsd ‘ 𝐽 )
30	25 29	eqeltrri	⊢ ℝ ∈ ( Clsd ‘ 𝐽 )
31		txcld	⊢ ( ( ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ∧ ℝ ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
32	24 30 31	sylancl	⊢ ( 𝑢 ∈ ℝ → ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
33	21 32	eqeltrd	⊢ ( 𝑢 ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
34	33	rgen	⊢ ∀ 𝑢 ∈ ℝ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
35		fnfvrnss	⊢ ( ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) Fn ℝ ∧ ∀ 𝑢 ∈ ℝ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) → ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
36	16 34 35	mp2an	⊢ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
37		ovex	⊢ ( 𝑓 [,) +∞ ) ∈ V
38	13 37	xpex	⊢ ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ V
39		eqid	⊢ ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) = ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) )
40	38 39	fnmpti	⊢ ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) Fn ℝ
41		oveq1	⊢ ( 𝑓 = 𝑣 → ( 𝑓 [,) +∞ ) = ( 𝑣 [,) +∞ ) )
42	41	xpeq2d	⊢ ( 𝑓 = 𝑣 → ( ℝ × ( 𝑓 [,) +∞ ) ) = ( ℝ × ( 𝑣 [,) +∞ ) ) )
43		ovex	⊢ ( 𝑣 [,) +∞ ) ∈ V
44	13 43	xpex	⊢ ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ V
45	42 39 44	fvmpt	⊢ ( 𝑣 ∈ ℝ → ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) = ( ℝ × ( 𝑣 [,) +∞ ) ) )
46		icopnfcld	⊢ ( 𝑣 ∈ ℝ → ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
47	46 23	eleqtrrdi	⊢ ( 𝑣 ∈ ℝ → ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) )
48		txcld	⊢ ( ( ℝ ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ) → ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
49	30 47 48	sylancr	⊢ ( 𝑣 ∈ ℝ → ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
50	45 49	eqeltrd	⊢ ( 𝑣 ∈ ℝ → ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
51	50	rgen	⊢ ∀ 𝑣 ∈ ℝ ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
52		fnfvrnss	⊢ ( ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) Fn ℝ ∧ ∀ 𝑣 ∈ ℝ ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) → ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
53	40 51 52	mp2an	⊢ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
54	36 53	unssi	⊢ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
55		fvex	⊢ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V
56		sssigagen	⊢ ( ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V → ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
57	55 56	ax-mp	⊢ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
58	54 57	sstri	⊢ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
59		sigagenss2	⊢ ( ( ∪ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∧ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) ∧ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V ) → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
60	11 58 55 59	mp3an	⊢ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )