Metamath Proof Explorer


Theorem salgensscntex

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)

Ref Expression
Hypotheses salgensscntex.a A=02
salgensscntex.s S=x𝒫A|xωAxω
salgensscntex.x X=rany01y
salgensscntex.g G=SalGenX
Assertion salgensscntex XSSSAlg¬GS

Proof

Step Hyp Ref Expression
1 salgensscntex.a A=02
2 salgensscntex.s S=x𝒫A|xωAxω
3 salgensscntex.x X=rany01y
4 salgensscntex.g G=SalGenX
5 0re 0
6 2re 2
7 5 6 pm3.2i 02
8 5 leidi 00
9 1le2 12
10 8 9 pm3.2i 0012
11 iccss 0200120102
12 7 10 11 mp2an 0102
13 id y01y01
14 12 13 sselid y01y02
15 14 1 eleqtrrdi y01yA
16 snelpwi yAy𝒫A
17 15 16 syl y01y𝒫A
18 snfi yFin
19 fict yFinyω
20 18 19 ax-mp yω
21 orc yωyωAyω
22 20 21 ax-mp yωAyω
23 22 a1i y01yωAyω
24 17 23 jca y01y𝒫AyωAyω
25 breq1 x=yxωyω
26 difeq2 x=yAx=Ay
27 26 breq1d x=yAxωAyω
28 25 27 orbi12d x=yxωAxωyωAyω
29 28 2 elrab2 ySy𝒫AyωAyω
30 24 29 sylibr y01yS
31 30 rgen y01yS
32 eqid y01y=y01y
33 32 rnmptss y01ySrany01yS
34 31 33 ax-mp rany01yS
35 3 34 eqsstri XS
36 ovex 02V
37 1 36 eqeltri AV
38 37 a1i AV
39 38 2 salexct SSAlg
40 39 mptru SSAlg
41 ovex 01V
42 41 mptex y01yV
43 42 rnex rany01yV
44 3 43 eqeltri XV
45 44 a1i XV
46 3 unieqi X=rany01y
47 snex yV
48 47 rgenw y01yV
49 dfiun3g y01yVy01y=rany01y
50 48 49 ax-mp y01y=rany01y
51 50 eqcomi rany01y=y01y
52 iunid y01y=01
53 46 51 52 3eqtrri 01=X
54 45 4 53 unisalgen 01G
55 54 mptru 01G
56 eqid 01=01
57 1 2 56 salexct2 ¬01S
58 nelss 01G¬01S¬GS
59 55 57 58 mp2an ¬GS
60 35 40 59 3pm3.2i XSSSAlg¬GS