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