Theorem salgensscntex 41085

Description: This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)

Hypotheses

Ref	Expression
salgensscntex.a	⊢ 𝐴 = (0[,]2)
salgensscntex.s	⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}
salgensscntex.x	⊢ 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})
salgensscntex.g	⊢ 𝐺 = (SalGen‘𝑋)

Assertion

Ref	Expression
salgensscntex	⊢ (𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ SAlg ∧ ¬ 𝐺 ⊆ 𝑆)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑆,𝑦

Allowed substitution hints:   𝐴(𝑦)   𝐺(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem salgensscntex

Step	Hyp	Ref	Expression
1		salgensscntex.x	. . 3 ⊢ 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})
2		0re 10263	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
3		2re 11313	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
4	2, 3	pm3.2i 457	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ ∧ 2 ∈ ℝ)
5	2	leidi 10785	. . . . . . . . . . . 12 ⊢ 0 ≤ 0
6		1le2 11465	. . . . . . . . . . . 12 ⊢ 1 ≤ 2
7	5, 6	pm3.2i 457	. . . . . . . . . . 11 ⊢ (0 ≤ 0 ∧ 1 ≤ 2)
8		iccss 12465	. . . . . . . . . . 11 ⊢ (((0 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (0 ≤ 0 ∧ 1 ≤ 2)) → (0[,]1) ⊆ (0[,]2))
9	4, 7, 8	mp2an 673	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ (0[,]2)
10		id 22	. . . . . . . . . 10 ⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈ (0[,]1))
11	9, 10	sseldi 3756	. . . . . . . . 9 ⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈ (0[,]2))
12		salgensscntex.a	. . . . . . . . 9 ⊢ 𝐴 = (0[,]2)
13	11, 12	syl6eleqr 2864	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → 𝑦 ∈ 𝐴)
14		snelpwi 5054	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴)
15	13, 14	syl 17	. . . . . . 7 ⊢ (𝑦 ∈ (0[,]1) → {𝑦} ∈ 𝒫 𝐴)
16		snfi 8215	. . . . . . . . . 10 ⊢ {𝑦} ∈ Fin
17		fict 8735	. . . . . . . . . 10 ⊢ ({𝑦} ∈ Fin → {𝑦} ≼ ω)
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ {𝑦} ≼ ω
19		orc 883	. . . . . . . . 9 ⊢ ({𝑦} ≼ ω → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
20	18, 19	ax-mp 5	. . . . . . . 8 ⊢ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)
21	20	a1i 11	. . . . . . 7 ⊢ (𝑦 ∈ (0[,]1) → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
22	15, 21	jca 502	. . . . . 6 ⊢ (𝑦 ∈ (0[,]1) → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
23		breq1 4800	. . . . . . . 8 ⊢ (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω))
24		difeq2 3880	. . . . . . . . 9 ⊢ (𝑥 = {𝑦} → (𝐴 ∖ 𝑥) = (𝐴 ∖ {𝑦}))
25	24	breq1d 4807	. . . . . . . 8 ⊢ (𝑥 = {𝑦} → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω))
26	23, 25	orbi12d 931	. . . . . . 7 ⊢ (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
27		salgensscntex.s	. . . . . . 7 ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}
28	26, 27	elrab2 3524	. . . . . 6 ⊢ ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
29	22, 28	sylibr 225	. . . . 5 ⊢ (𝑦 ∈ (0[,]1) → {𝑦} ∈ 𝑆)
30	29	rgen 3074	. . . 4 ⊢ ∀𝑦 ∈ (0[,]1){𝑦} ∈ 𝑆
31		eqid 2774	. . . . 5 ⊢ (𝑦 ∈ (0[,]1) ↦ {𝑦}) = (𝑦 ∈ (0[,]1) ↦ {𝑦})
32	31	rnmptss 6552	. . . 4 ⊢ (∀𝑦 ∈ (0[,]1){𝑦} ∈ 𝑆 → ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) ⊆ 𝑆)
33	30, 32	ax-mp 5	. . 3 ⊢ ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) ⊆ 𝑆
34	1, 33	eqsstri 3791	. 2 ⊢ 𝑋 ⊆ 𝑆
35		ovex 6844	. . . . . 6 ⊢ (0[,]2) ∈ V
36	12, 35	eqeltri 2849	. . . . 5 ⊢ 𝐴 ∈ V
37	36	a1i 11	. . . 4 ⊢ (⊤ → 𝐴 ∈ V)
38	37, 27	salexct 41075	. . 3 ⊢ (⊤ → 𝑆 ∈ SAlg)
39	38	trud 1644	. 2 ⊢ 𝑆 ∈ SAlg
40		ovex 6844	. . . . . . . . 9 ⊢ (0[,]1) ∈ V
41	40	mptex 6649	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) ↦ {𝑦}) ∈ V
42	41	rnex 7268	. . . . . . 7 ⊢ ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) ∈ V
43	1, 42	eqeltri 2849	. . . . . 6 ⊢ 𝑋 ∈ V
44	43	a1i 11	. . . . 5 ⊢ (⊤ → 𝑋 ∈ V)
45		salgensscntex.g	. . . . 5 ⊢ 𝐺 = (SalGen‘𝑋)
46	1	unieqi 4594	. . . . . 6 ⊢ ∪ 𝑋 = ∪ ran (𝑦 ∈ (0[,]1) ↦ {𝑦})
47		snex 5050	. . . . . . . . 9 ⊢ {𝑦} ∈ V
48	47	rgenw 3076	. . . . . . . 8 ⊢ ∀𝑦 ∈ (0[,]1){𝑦} ∈ V
49		dfiun3g 5528	. . . . . . . 8 ⊢ (∀𝑦 ∈ (0[,]1){𝑦} ∈ V → ∪ 𝑦 ∈ (0[,]1){𝑦} = ∪ ran (𝑦 ∈ (0[,]1) ↦ {𝑦}))
50	48, 49	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑦 ∈ (0[,]1){𝑦} = ∪ ran (𝑦 ∈ (0[,]1) ↦ {𝑦})
51	50	eqcomi 2783	. . . . . 6 ⊢ ∪ ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) = ∪ 𝑦 ∈ (0[,]1){𝑦}
52		iunid 4720	. . . . . 6 ⊢ ∪ 𝑦 ∈ (0[,]1){𝑦} = (0[,]1)
53	46, 51, 52	3eqtrri 2801	. . . . 5 ⊢ (0[,]1) = ∪ 𝑋
54	44, 45, 53	unisalgen 41081	. . . 4 ⊢ (⊤ → (0[,]1) ∈ 𝐺)
55	54	trud 1644	. . 3 ⊢ (0[,]1) ∈ 𝐺
56		eqid 2774	. . . 4 ⊢ (0[,]1) = (0[,]1)
57	12, 27, 56	salexct2 41080	. . 3 ⊢ ¬ (0[,]1) ∈ 𝑆
58		nelss 3820	. . 3 ⊢ (((0[,]1) ∈ 𝐺 ∧ ¬ (0[,]1) ∈ 𝑆) → ¬ 𝐺 ⊆ 𝑆)
59	55, 57, 58	mp2an 673	. 2 ⊢ ¬ 𝐺 ⊆ 𝑆
60	34, 39, 59	3pm3.2i 1429	1 ⊢ (𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ SAlg ∧ ¬ 𝐺 ⊆ 𝑆)

Syntax hints:  ¬ wn 3   ∧ wa 383   ∨ wo 863   ∧ w3a 1098   = wceq 1634  ⊤wtru 1635   ∈ wcel 2148  ∀wral 3064  {crab 3068  Vcvv 3355   ∖ cdif 3726   ⊆ wss 3729  𝒫 cpw 4307  {csn 4326  ∪ cuni 4585  ∪ ciun 4665   class class class wbr 4797   ↦ cmpt 4876  ran crn 5264  ‘cfv 6042  (class class class)co 6812  ωcom 7233   ≼ cdom 8128  Fincfn 8130  ℝcr 10158  0cc0 10159  1c1 10160   ≤ cle 10298  2c2 11293  [,]cicc 12402  SAlgcsalg 41051  SalGencsalgen 41055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-inf2 8723  ax-cc 9480  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-fal 1640  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-1st 7336  df-2nd 7337  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-omul 7739  df-er 7917  df-map 8032  df-pm 8033  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-sup 8525  df-inf 8526  df-oi 8592  df-card 8986  df-acn 8989  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-n0 11517  df-z 11602  df-uz 11911  df-q 12014  df-rp 12053  df-xneg 12168  df-xadd 12169  df-xmul 12170  df-ioo 12403  df-ioc 12404  df-ico 12405  df-icc 12406  df-fz 12556  df-fzo 12696  df-fl 12823  df-seq 13031  df-exp 13090  df-hash 13344  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-limsup 14432  df-clim 14449  df-rlim 14450  df-sum 14647  df-topgen 16332  df-psmet 19973  df-xmet 19974  df-met 19975  df-bl 19976  df-mopn 19977  df-top 20939  df-topon 20956  df-bases 20991  df-ntr 21065  df-salg 41052  df-salgen 41056

This theorem is referenced by: (None)