sxbrsigalem2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sxbrsigalem2		Structured version Unicode version

Theorem sxbrsigalem2 29117

Description: The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of

is a subset of the sigma-algebra generated by the closed half-spaces of

. The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (Contributed by Thierry Arnoux, 17-Sep-2017.)

**Hypotheses**
Ref	Expression
sxbrsiga.0
dya2ioc.1
dya2ioc.2

**Assertion**
Ref	Expression
sxbrsigalem2	sigaGen sigaGen

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem sxbrsigalem2 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sxbrsiga.0	. . . 4
2		dya2ioc.1	. . . 4
3		dya2ioc.2	. . . 4
4	1, 2, 3	dya2iocucvr 29115	. . 3
5		sxbrsigalem0 29102	. . 3
6	4, 5	eqtr4i 2454	. 2
7		vex 3083	. . . . . 6
8		vex 3083	. . . . . 6
9	7, 8	xpex 6610	. . . . 5
10	3, 9	elrnmpt2 6424	. . . 4
11		simpr 462	. . . . . . 7 $/\$ $/\$
12	1, 2	dya2icobrsiga 29107	. . . . . . . . . . . . 13 𝔅_ℝ
13		brsigasspwrn 29016	. . . . . . . . . . . . 13 𝔅_ℝ
14	12, 13	sstri 3473	. . . . . . . . . . . 12
15	14	sseli 3460	. . . . . . . . . . 11
16	15	elpwid 3991	. . . . . . . . . 10
17	14	sseli 3460	. . . . . . . . . . 11
18	17	elpwid 3991	. . . . . . . . . 10
19		xpinpreima2 28722	. . . . . . . . . 10 $/\$
20	16, 18, 19	syl2an 479	. . . . . . . . 9 $/\$
21		reex 9638	. . . . . . . . . . . . . . . . 17
22	21	mptex 6152	. . . . . . . . . . . . . . . 16
23	22	rnex 6742	. . . . . . . . . . . . . . 15
24	21	mptex 6152	. . . . . . . . . . . . . . . 16
25	24	rnex 6742	. . . . . . . . . . . . . . 15
26	23, 25	unex 6604	. . . . . . . . . . . . . 14
27	26	a1i 11	. . . . . . . . . . . . 13
28	27	sgsiga 28973	. . . . . . . . . . . 12 sigaGen sigAlgebra
29	28	trud 1446	. . . . . . . . . . 11 sigaGen sigAlgebra
30	29	a1i 11	. . . . . . . . . 10 $/\$ sigaGen sigAlgebra
31		1stpreima 28290	. . . . . . . . . . . . 13
32	16, 31	syl 17	. . . . . . . . . . . 12
33		ovex 6334	. . . . . . . . . . . . . 14
34	2, 33	elrnmpt2 6424	. . . . . . . . . . . . 13
35		simpr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
36	35	xpeq1d 4876	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37		difxp1 5281	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
38		simpl 458	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	zred 11048	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40		2rp 11315	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
42		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
43	41, 42	rpexpcld 12446	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
44	39, 43	rerpdivcld 11377	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
45	44	rexrd 9698	. . . . . . . . . . . . . . . . . . . . 21 $/\$
46		1red 9666	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
47	39, 46	readdcld 9678	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
48	47, 43	rerpdivcld 11377	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
49	48	rexrd 9698	. . . . . . . . . . . . . . . . . . . . 21 $/\$
50		pnfxr 11420	. . . . . . . . . . . . . . . . . . . . . 22
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
52	39	lep1d 10546	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
53	39, 47, 43, 52	lediv1dd 11404	. . . . . . . . . . . . . . . . . . . . 21 $/\$
54		pnfge 11440	. . . . . . . . . . . . . . . . . . . . . 22
55	49, 54	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
56		difico 28372	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\$
57	45, 49, 51, 53, 55, 56	syl32anc 1272	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$
58	57	xpeq1d 4876	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
59	37, 58	syl5reqr 2478	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
60	29	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ sigaGen sigAlgebra
61		ssun1 3629	. . . . . . . . . . . . . . . . . . . . 21
62		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . 23
63		oveq1 6313	. . . . . . . . . . . . . . . . . . . . . . . . . 26
64	63	xpeq1d 4876	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	64	eqeq2d 2436	. . . . . . . . . . . . . . . . . . . . . . . 24
66	65	rspcev 3182	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
67	44, 62, 66	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
68		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . 23
69		ovex 6334	. . . . . . . . . . . . . . . . . . . . . . . 24
70	69, 21	xpex 6610	. . . . . . . . . . . . . . . . . . . . . . 23
71	68, 70	elrnmpti 5104	. . . . . . . . . . . . . . . . . . . . . 22
72	67, 71	sylibr 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$
73	61, 72	sseldi 3462	. . . . . . . . . . . . . . . . . . . 20 $/\$
74		elsigagen 28978	. . . . . . . . . . . . . . . . . . . 20 $/\$ sigaGen
75	26, 73, 74	sylancr 667	. . . . . . . . . . . . . . . . . . 19 $/\$ sigaGen
76		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . 23
77		oveq1 6313	. . . . . . . . . . . . . . . . . . . . . . . . . 26
78	77	xpeq1d 4876	. . . . . . . . . . . . . . . . . . . . . . . . 25
79	78	eqeq2d 2436	. . . . . . . . . . . . . . . . . . . . . . . 24
80	79	rspcev 3182	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
81	48, 76, 80	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
82	68, 70	elrnmpti 5104	. . . . . . . . . . . . . . . . . . . . . 22
83	81, 82	sylibr 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$
84	61, 83	sseldi 3462	. . . . . . . . . . . . . . . . . . . 20 $/\$
85		elsigagen 28978	. . . . . . . . . . . . . . . . . . . 20 $/\$ sigaGen
86	26, 84, 85	sylancr 667	. . . . . . . . . . . . . . . . . . 19 $/\$ sigaGen
87		difelsiga 28964	. . . . . . . . . . . . . . . . . . 19 sigaGen sigAlgebra $/\$ sigaGen $/\$ sigaGen $\$ sigaGen
88	60, 75, 86, 87	syl3anc 1264	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ sigaGen
89	59, 88	eqeltrd 2507	. . . . . . . . . . . . . . . . 17 $/\$ sigaGen
90	89	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ sigaGen
91	36, 90	eqeltrd 2507	. . . . . . . . . . . . . . 15 $/\$ $/\$ sigaGen
92	91	ex 435	. . . . . . . . . . . . . 14 $/\$ sigaGen
93	92	rexlimivv 2919	. . . . . . . . . . . . 13 sigaGen
94	34, 93	sylbi 198	. . . . . . . . . . . 12 sigaGen
95	32, 94	eqeltrd 2507	. . . . . . . . . . 11 sigaGen
96	95	adantr 466	. . . . . . . . . 10 $/\$ sigaGen
97		2ndpreima 28291	. . . . . . . . . . . . 13
98	18, 97	syl 17	. . . . . . . . . . . 12
99	2, 33	elrnmpt2 6424	. . . . . . . . . . . . 13
100		simpr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
101	100	xpeq2d 4877	. . . . . . . . . . . . . . . 16 $/\$ $/\$
102		difxp2 5282	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
103	57	xpeq2d 4877	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
104	102, 103	syl5reqr 2478	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
105		ssun2 3630	. . . . . . . . . . . . . . . . . . . . 21
106		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . 23
107		oveq1 6313	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	xpeq2d 4877	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	108	eqeq2d 2436	. . . . . . . . . . . . . . . . . . . . . . . 24
110	109	rspcev 3182	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
111	44, 106, 110	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
112		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . 23
113		ovex 6334	. . . . . . . . . . . . . . . . . . . . . . . 24
114	21, 113	xpex 6610	. . . . . . . . . . . . . . . . . . . . . . 23
115	112, 114	elrnmpti 5104	. . . . . . . . . . . . . . . . . . . . . 22
116	111, 115	sylibr 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	105, 116	sseldi 3462	. . . . . . . . . . . . . . . . . . . 20 $/\$
118		elsigagen 28978	. . . . . . . . . . . . . . . . . . . 20 $/\$ sigaGen
119	26, 117, 118	sylancr 667	. . . . . . . . . . . . . . . . . . 19 $/\$ sigaGen
120		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . 23
121		oveq1 6313	. . . . . . . . . . . . . . . . . . . . . . . . . 26
122	121	xpeq2d 4877	. . . . . . . . . . . . . . . . . . . . . . . . 25
123	122	eqeq2d 2436	. . . . . . . . . . . . . . . . . . . . . . . 24
124	123	rspcev 3182	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125	48, 120, 124	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
126	112, 114	elrnmpti 5104	. . . . . . . . . . . . . . . . . . . . . 22
127	125, 126	sylibr 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$
128	105, 127	sseldi 3462	. . . . . . . . . . . . . . . . . . . 20 $/\$
129		elsigagen 28978	. . . . . . . . . . . . . . . . . . . 20 $/\$ sigaGen
130	26, 128, 129	sylancr 667	. . . . . . . . . . . . . . . . . . 19 $/\$ sigaGen
131		difelsiga 28964	. . . . . . . . . . . . . . . . . . 19 sigaGen sigAlgebra $/\$ sigaGen $/\$ sigaGen $\$ sigaGen
132	60, 119, 130, 131	syl3anc 1264	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ sigaGen
133	104, 132	eqeltrd 2507	. . . . . . . . . . . . . . . . 17 $/\$ sigaGen
134	133	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ sigaGen
135	101, 134	eqeltrd 2507	. . . . . . . . . . . . . . 15 $/\$ $/\$ sigaGen
136	135	ex 435	. . . . . . . . . . . . . 14 $/\$ sigaGen
137	136	rexlimivv 2919	. . . . . . . . . . . . 13 sigaGen
138	99, 137	sylbi 198	. . . . . . . . . . . 12 sigaGen
139	98, 138	eqeltrd 2507	. . . . . . . . . . 11 sigaGen
140	139	adantl 467	. . . . . . . . . 10 $/\$ sigaGen
141		inelsiga 28966	. . . . . . . . . 10 sigaGen sigAlgebra $/\$ sigaGen $/\$ sigaGen sigaGen
142	30, 96, 140, 141	syl3anc 1264	. . . . . . . . 9 $/\$ sigaGen
143	20, 142	eqeltrd 2507	. . . . . . . 8 $/\$ sigaGen
144	143	adantr 466	. . . . . . 7 $/\$ $/\$ sigaGen
145	11, 144	eqeltrd 2507	. . . . . 6 $/\$ $/\$ sigaGen
146	145	ex 435	. . . . 5 $/\$ sigaGen
147	146	rexlimivv 2919	. . . 4 sigaGen
148	10, 147	sylbi 198	. . 3 sigaGen
149	148	ssriv 3468	. 2 sigaGen
150		sigagenss2 28981	. 2 $/\$ sigaGen $/\$ sigaGen sigaGen
151	6, 149, 26, 150	mp3an 1360	1 sigaGen sigaGen

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 370

wceq 1437

wtru 1438

wcel 1872

wrex 2772

cvv 3080 $\$ cdif 3433

cun 3434

cin 3435

wss 3436

cpw 3981

cuni 4219 class class class wbr 4423

cmpt 4482

cxp 4851

ccnv 4852

crn 4854

cres 4855

cima 4856

cfv 5601 (class class class)co 6306

cmpt2 6308

c1st 6806

c2nd 6807

cr 9546

c1 9548

caddc 9550

cpnf 9680

cxr 9682

cle 9684

cdiv 10277

c2 10667

cz 10945

crp 11310

cioo 11643

cico 11645

cexp 12279

ctg 15336 sigAlgebracsiga 28938 sigaGencsigagen 28969 𝔅_ℝcbrsiga 29012

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6598 ax-inf2 8156 ax-ac2 8901 ax-cnex 9603 ax-resscn 9604 ax-1cn 9605 ax-icn 9606 ax-addcl 9607 ax-addrcl 9608 ax-mulcl 9609 ax-mulrcl 9610 ax-mulcom 9611 ax-addass 9612 ax-mulass 9613 ax-distr 9614 ax-i2m1 9615 ax-1ne0 9616 ax-1rid 9617 ax-rnegex 9618 ax-rrecex 9619 ax-cnre 9620 ax-pre-lttri 9621 ax-pre-lttrn 9622 ax-pre-ltadd 9623 ax-pre-mulgt0 9624 ax-pre-sup 9625 ax-addf 9626 ax-mulf 9627

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-iin 4302 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6268 df-ov 6309 df-oprab 6310 df-mpt2 6311 df-of 6546 df-om 6708 df-1st 6808 df-2nd 6809 df-supp 6927 df-wrecs 7040 df-recs 7102 df-rdg 7140 df-1o 7194 df-2o 7195 df-oadd 7198 df-er 7375 df-map 7486 df-pm 7487 df-ixp 7535 df-en 7582 df-dom 7583 df-sdom 7584 df-fin 7585 df-fsupp 7894 df-fi 7935 df-sup 7966 df-inf 7967 df-oi 8035 df-card 8382 df-acn 8385 df-ac 8555 df-cda 8606 df-pnf 9685 df-mnf 9686 df-xr 9687 df-ltxr 9688 df-le 9689 df-sub 9870 df-neg 9871 df-div 10278 df-nn 10618 df-2 10676 df-3 10677 df-4 10678 df-5 10679 df-6 10680 df-7 10681 df-8 10682 df-9 10683 df-10 10684 df-n0 10878 df-z 10946 df-dec 11060 df-uz 11168 df-q 11273 df-rp 11311 df-xneg 11417 df-xadd 11418 df-xmul 11419 df-ioo 11647 df-ioc 11648 df-ico 11649 df-icc 11650 df-fz 11793 df-fzo 11924 df-fl 12035 df-mod 12104 df-seq 12221 df-exp 12280 df-fac 12467 df-bc 12495 df-hash 12523 df-shft 13131 df-cj 13163 df-re 13164 df-im 13165 df-sqrt 13299 df-abs 13300 df-limsup 13526 df-clim 13552 df-rlim 13553 df-sum 13753 df-ef 14121 df-sin 14123 df-cos 14124 df-pi 14126 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-fbas 18967 df-fg 18968 df-cnfld 18971 df-refld 19172 df-top 19920 df-bases 19921 df-topon 19922 df-topsp 19923 df-cld 20033 df-ntr 20034 df-cls 20035 df-nei 20113 df-lp 20151 df-perf 20152 df-cn 20242 df-cnp 20243 df-haus 20330 df-cmp 20401 df-tx 20576 df-hmeo 20769 df-fil 20860 df-fm 20952 df-flim 20953 df-flf 20954 df-fcls 20955 df-xms 21334 df-ms 21335 df-tms 21336 df-cncf 21909 df-cfil 22224 df-cmet 22226 df-cms 22302 df-limc 22820 df-dv 22821 df-log 23505 df-cxp 23506 df-logb 23701 df-siga 28939 df-sigagen 28970 df-brsiga 29013

This theorem is referenced by: sxbrsigalem4 29118

W3C validator