Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  salgensscntex Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 salgensscntex.x . . 3 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})
2 0re 10263 . . . . . . . . . . . 12 0 ∈ ℝ
3 2re 11313 . . . . . . . . . . . 12 2 ∈ ℝ
42, 3pm3.2i 457 . . . . . . . . . . 11 (0 ∈ ℝ ∧ 2 ∈ ℝ)
52leidi 10785 . . . . . . . . . . . 12 0 ≤ 0
6 1le2 11465 . . . . . . . . . . . 12 1 ≤ 2
75, 6pm3.2i 457 . . . . . . . . . . 11 (0 ≤ 0 ∧ 1 ≤ 2)
8 iccss 12465 . . . . . . . . . . 11 (((0 ∈ ℝ ∧ 2 ∈ ℝ) ∧ (0 ≤ 0 ∧ 1 ≤ 2)) → (0[,]1) ⊆ (0[,]2))
94, 7, 8mp2an 673 . . . . . . . . . 10 (0[,]1) ⊆ (0[,]2)
10 id 22 . . . . . . . . . 10 (𝑦 ∈ (0[,]1) → 𝑦 ∈ (0[,]1))
119, 10sseldi 3756 . . . . . . . . 9 (𝑦 ∈ (0[,]1) → 𝑦 ∈ (0[,]2))
12 salgensscntex.a . . . . . . . . 9 𝐴 = (0[,]2)
1311, 12syl6eleqr 2864 . . . . . . . 8 (𝑦 ∈ (0[,]1) → 𝑦𝐴)
14 snelpwi 5054 . . . . . . . 8 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
1513, 14syl 17 . . . . . . 7 (𝑦 ∈ (0[,]1) → {𝑦} ∈ 𝒫 𝐴)
16 snfi 8215 . . . . . . . . . 10 {𝑦} ∈ Fin
17 fict 8735 . . . . . . . . . 10 ({𝑦} ∈ Fin → {𝑦} ≼ ω)
1816, 17ax-mp 5 . . . . . . . . 9 {𝑦} ≼ ω
19 orc 883 . . . . . . . . 9 ({𝑦} ≼ ω → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
2018, 19ax-mp 5 . . . . . . . 8 ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)
2120a1i 11 . . . . . . 7 (𝑦 ∈ (0[,]1) → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
2215, 21jca 502 . . . . . 6 (𝑦 ∈ (0[,]1) → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
23 breq1 4800 . . . . . . . 8 (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω))
24 difeq2 3880 . . . . . . . . 9 (𝑥 = {𝑦} → (𝐴𝑥) = (𝐴 ∖ {𝑦}))
2524breq1d 4807 . . . . . . . 8 (𝑥 = {𝑦} → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω))
2623, 25orbi12d 931 . . . . . . 7 (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
27 salgensscntex.s . . . . . . 7 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)}
2826, 27elrab2 3524 . . . . . 6 ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
2922, 28sylibr 225 . . . . 5 (𝑦 ∈ (0[,]1) → {𝑦} ∈ 𝑆)
3029rgen 3074 . . . 4 𝑦 ∈ (0[,]1){𝑦} ∈ 𝑆
31 eqid 2774 . . . . 5 (𝑦 ∈ (0[,]1) ↦ {𝑦}) = (𝑦 ∈ (0[,]1) ↦ {𝑦})
3231rnmptss 6552 . . . 4 (∀𝑦 ∈ (0[,]1){𝑦} ∈ 𝑆 → ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) ⊆ 𝑆)
3330, 32ax-mp 5 . . 3 ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) ⊆ 𝑆
341, 33eqsstri 3791 . 2 𝑋𝑆
35 ovex 6844 . . . . . 6 (0[,]2) ∈ V
3612, 35eqeltri 2849 . . . . 5 𝐴 ∈ V
3736a1i 11 . . . 4 (⊤ → 𝐴 ∈ V)
3837, 27salexct 41075 . . 3 (⊤ → 𝑆 ∈ SAlg)
3938trud 1644 . 2 𝑆 ∈ SAlg
40 ovex 6844 . . . . . . . . 9 (0[,]1) ∈ V
4140mptex 6649 . . . . . . . 8 (𝑦 ∈ (0[,]1) ↦ {𝑦}) ∈ V
4241rnex 7268 . . . . . . 7 ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) ∈ V
431, 42eqeltri 2849 . . . . . 6 𝑋 ∈ V
4443a1i 11 . . . . 5 (⊤ → 𝑋 ∈ V)
45 salgensscntex.g . . . . 5 𝐺 = (SalGen‘𝑋)
461unieqi 4594 . . . . . 6 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})
47 snex 5050 . . . . . . . . 9 {𝑦} ∈ V
4847rgenw 3076 . . . . . . . 8 𝑦 ∈ (0[,]1){𝑦} ∈ V
49 dfiun3g 5528 . . . . . . . 8 (∀𝑦 ∈ (0[,]1){𝑦} ∈ V → 𝑦 ∈ (0[,]1){𝑦} = ran (𝑦 ∈ (0[,]1) ↦ {𝑦}))
5048, 49ax-mp 5 . . . . . . 7 𝑦 ∈ (0[,]1){𝑦} = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})
5150eqcomi 2783 . . . . . 6 ran (𝑦 ∈ (0[,]1) ↦ {𝑦}) = 𝑦 ∈ (0[,]1){𝑦}
52 iunid 4720 . . . . . 6 𝑦 ∈ (0[,]1){𝑦} = (0[,]1)
5346, 51, 523eqtrri 2801 . . . . 5 (0[,]1) = 𝑋
5444, 45, 53unisalgen 41081 . . . 4 (⊤ → (0[,]1) ∈ 𝐺)
5554trud 1644 . . 3 (0[,]1) ∈ 𝐺
56 eqid 2774 . . . 4 (0[,]1) = (0[,]1)
5712, 27, 56salexct2 41080 . . 3 ¬ (0[,]1) ∈ 𝑆
58 nelss 3820 . . 3 (((0[,]1) ∈ 𝐺 ∧ ¬ (0[,]1) ∈ 𝑆) → ¬ 𝐺𝑆)
5955, 57, 58mp2an 673 . 2 ¬ 𝐺𝑆
6034, 39, 593pm3.2i 1429 1 (𝑋𝑆𝑆 ∈ SAlg ∧ ¬ 𝐺𝑆)
Colors of variables: wff setvar class
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)
  Copyright terms: Public domain W3C validator