Metamath Proof Explorer


Theorem dfsalgen2

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 φ X V
Assertion dfsalgen2 φ SalGen X = S S SAlg S = X X S y SAlg y = X X y S y

Proof

Step Hyp Ref Expression
1 dfsalgen2.1 φ X V
2 id SalGen X = S SalGen X = S
3 2 eqcomd SalGen X = S S = SalGen X
4 3 adantl φ SalGen X = S S = SalGen X
5 salgencl X V SalGen X SAlg
6 1 5 syl φ SalGen X SAlg
7 6 adantr φ SalGen X = S SalGen X SAlg
8 4 7 eqeltrd φ SalGen X = S S SAlg
9 unieq SalGen X = S SalGen X = S
10 9 adantl φ SalGen X = S SalGen X = S
11 1 adantr φ SalGen X = S X V
12 eqid SalGen X = SalGen X
13 eqid X = X
14 11 12 13 salgenuni φ SalGen X = S SalGen X = X
15 10 14 eqtr3d φ SalGen X = S S = X
16 12 sssalgen X V X SalGen X
17 11 16 syl φ SalGen X = S X SalGen X
18 simpr φ SalGen X = S SalGen X = S
19 17 18 sseqtrd φ SalGen X = S X S
20 8 15 19 3jca φ SalGen X = S S SAlg S = X X S
21 4 ad2antrr φ SalGen X = S y SAlg X y S = SalGen X
22 21 adantrl φ SalGen X = S y SAlg y = X X y S = SalGen X
23 11 ad2antrr φ SalGen X = S y SAlg X y X V
24 23 adantrl φ SalGen X = S y SAlg y = X X y X V
25 simplr φ SalGen X = S y SAlg X y y SAlg
26 25 adantrl φ SalGen X = S y SAlg y = X X y y SAlg
27 simpr φ SalGen X = S y SAlg X y X y
28 27 adantrl φ SalGen X = S y SAlg y = X X y X y
29 simprl φ SalGen X = S y SAlg y = X X y y = X
30 24 12 26 28 29 salgenss φ SalGen X = S y SAlg y = X X y SalGen X y
31 22 30 eqsstrd φ SalGen X = S y SAlg y = X X y S y
32 31 ex φ SalGen X = S y SAlg y = X X y S y
33 32 ralrimiva φ SalGen X = S y SAlg y = X X y S y
34 20 33 jca φ SalGen X = S S SAlg S = X X S y SAlg y = X X y S y
35 34 ex φ SalGen X = S S SAlg S = X X S y SAlg y = X X y S y
36 1 adantr φ S SAlg S = X X S y SAlg y = X X y S y X V
37 simprl1 φ S SAlg S = X X S y SAlg y = X X y S y S SAlg
38 simprl2 φ S SAlg S = X X S y SAlg y = X X y S y S = X
39 simprl3 φ S SAlg S = X X S y SAlg y = X X y S y X S
40 unieq y = w y = w
41 40 eqeq1d y = w y = X w = X
42 sseq2 y = w X y X w
43 41 42 anbi12d y = w y = X X y w = X X w
44 sseq2 y = w S y S w
45 43 44 imbi12d y = w y = X X y S y w = X X w S w
46 45 cbvralvw y SAlg y = X X y S y w SAlg w = X X w S w
47 46 biimpi y SAlg y = X X y S y w SAlg w = X X w S w
48 47 adantr y SAlg y = X X y S y w SAlg w SAlg w = X X w S w
49 simpr y SAlg y = X X y S y w SAlg w SAlg
50 48 49 jca y SAlg y = X X y S y w SAlg w SAlg w = X X w S w w SAlg
51 50 3ad2antr1 y SAlg y = X X y S y w SAlg w = X X w w SAlg w = X X w S w w SAlg
52 3simpc w SAlg w = X X w w = X X w
53 52 adantl y SAlg y = X X y S y w SAlg w = X X w w = X X w
54 rspa w SAlg w = X X w S w w SAlg w = X X w S w
55 51 53 54 sylc y SAlg y = X X y S y w SAlg w = X X w S w
56 55 adantll S SAlg S = X X S y SAlg y = X X y S y w SAlg w = X X w S w
57 56 adantll φ S SAlg S = X X S y SAlg y = X X y S y w SAlg w = X X w S w
58 36 37 38 39 57 issalgend φ S SAlg S = X X S y SAlg y = X X y S y SalGen X = S
59 58 ex φ S SAlg S = X X S y SAlg y = X X y S y SalGen X = S
60 35 59 impbid φ SalGen X = S S SAlg S = X X S y SAlg y = X X y S y