Description: Alternate characterization of the sigma-algebra generated by a set. It is the smallest sigma-algebra, on the same base set, that includes the set. (Contributed by Glauco Siliprandi, 3-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dfsalgen2.1 | |
|
Assertion | dfsalgen2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsalgen2.1 | |
|
2 | id | |
|
3 | 2 | eqcomd | |
4 | 3 | adantl | |
5 | salgencl | |
|
6 | 1 5 | syl | |
7 | 6 | adantr | |
8 | 4 7 | eqeltrd | |
9 | unieq | |
|
10 | 9 | adantl | |
11 | 1 | adantr | |
12 | eqid | |
|
13 | eqid | |
|
14 | 11 12 13 | salgenuni | |
15 | 10 14 | eqtr3d | |
16 | 12 | sssalgen | |
17 | 11 16 | syl | |
18 | simpr | |
|
19 | 17 18 | sseqtrd | |
20 | 8 15 19 | 3jca | |
21 | 4 | ad2antrr | |
22 | 21 | adantrl | |
23 | 11 | ad2antrr | |
24 | 23 | adantrl | |
25 | simplr | |
|
26 | 25 | adantrl | |
27 | simpr | |
|
28 | 27 | adantrl | |
29 | simprl | |
|
30 | 24 12 26 28 29 | salgenss | |
31 | 22 30 | eqsstrd | |
32 | 31 | ex | |
33 | 32 | ralrimiva | |
34 | 20 33 | jca | |
35 | 34 | ex | |
36 | 1 | adantr | |
37 | simprl1 | |
|
38 | simprl2 | |
|
39 | simprl3 | |
|
40 | unieq | |
|
41 | 40 | eqeq1d | |
42 | sseq2 | |
|
43 | 41 42 | anbi12d | |
44 | sseq2 | |
|
45 | 43 44 | imbi12d | |
46 | 45 | cbvralvw | |
47 | 46 | biimpi | |
48 | 47 | adantr | |
49 | simpr | |
|
50 | 48 49 | jca | |
51 | 50 | 3ad2antr1 | |
52 | 3simpc | |
|
53 | 52 | adantl | |
54 | rspa | |
|
55 | 51 53 54 | sylc | |
56 | 55 | adantll | |
57 | 56 | adantll | |
58 | 36 37 38 39 57 | issalgend | |
59 | 58 | ex | |
60 | 35 59 | impbid | |