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 = 0 2
salgensscntex.s S = x 𝒫 A | x ω A x ω
salgensscntex.x X = ran y 0 1 y
salgensscntex.g G = SalGen X
Assertion salgensscntex X S S SAlg ¬ G S

Proof

Step Hyp Ref Expression
1 salgensscntex.a A = 0 2
2 salgensscntex.s S = x 𝒫 A | x ω A x ω
3 salgensscntex.x X = ran y 0 1 y
4 salgensscntex.g G = SalGen X
5 0re 0
6 2re 2
7 5 6 pm3.2i 0 2
8 5 leidi 0 0
9 1le2 1 2
10 8 9 pm3.2i 0 0 1 2
11 iccss 0 2 0 0 1 2 0 1 0 2
12 7 10 11 mp2an 0 1 0 2
13 id y 0 1 y 0 1
14 12 13 sseldi y 0 1 y 0 2
15 14 1 eleqtrrdi y 0 1 y A
16 snelpwi y A y 𝒫 A
17 15 16 syl y 0 1 y 𝒫 A
18 snfi y Fin
19 fict y Fin y ω
20 18 19 ax-mp y ω
21 orc y ω y ω A y ω
22 20 21 ax-mp y ω A y ω
23 22 a1i y 0 1 y ω A y ω
24 17 23 jca y 0 1 y 𝒫 A y ω A y ω
25 breq1 x = y x ω y ω
26 difeq2 x = y A x = A y
27 26 breq1d x = y A x ω A y ω
28 25 27 orbi12d x = y x ω A x ω y ω A y ω
29 28 2 elrab2 y S y 𝒫 A y ω A y ω
30 24 29 sylibr y 0 1 y S
31 30 rgen y 0 1 y S
32 eqid y 0 1 y = y 0 1 y
33 32 rnmptss y 0 1 y S ran y 0 1 y S
34 31 33 ax-mp ran y 0 1 y S
35 3 34 eqsstri X S
36 ovex 0 2 V
37 1 36 eqeltri A V
38 37 a1i A V
39 38 2 salexct S SAlg
40 39 mptru S SAlg
41 ovex 0 1 V
42 41 mptex y 0 1 y V
43 42 rnex ran y 0 1 y V
44 3 43 eqeltri X V
45 44 a1i X V
46 3 unieqi X = ran y 0 1 y
47 snex y V
48 47 rgenw y 0 1 y V
49 dfiun3g y 0 1 y V y 0 1 y = ran y 0 1 y
50 48 49 ax-mp y 0 1 y = ran y 0 1 y
51 50 eqcomi ran y 0 1 y = y 0 1 y
52 iunid y 0 1 y = 0 1
53 46 51 52 3eqtrri 0 1 = X
54 45 4 53 unisalgen 0 1 G
55 54 mptru 0 1 G
56 eqid 0 1 = 0 1
57 1 2 56 salexct2 ¬ 0 1 S
58 nelss 0 1 G ¬ 0 1 S ¬ G S
59 55 57 58 mp2an ¬ G S
60 35 40 59 3pm3.2i X S S SAlg ¬ G S