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 φXV
Assertion dfsalgen2 φSalGenX=SSSAlgS=XXSySAlgy=XXySy

Proof

Step Hyp Ref Expression
1 dfsalgen2.1 φXV
2 id SalGenX=SSalGenX=S
3 2 eqcomd SalGenX=SS=SalGenX
4 3 adantl φSalGenX=SS=SalGenX
5 salgencl XVSalGenXSAlg
6 1 5 syl φSalGenXSAlg
7 6 adantr φSalGenX=SSalGenXSAlg
8 4 7 eqeltrd φSalGenX=SSSAlg
9 unieq SalGenX=SSalGenX=S
10 9 adantl φSalGenX=SSalGenX=S
11 1 adantr φSalGenX=SXV
12 eqid SalGenX=SalGenX
13 eqid X=X
14 11 12 13 salgenuni φSalGenX=SSalGenX=X
15 10 14 eqtr3d φSalGenX=SS=X
16 12 sssalgen XVXSalGenX
17 11 16 syl φSalGenX=SXSalGenX
18 simpr φSalGenX=SSalGenX=S
19 17 18 sseqtrd φSalGenX=SXS
20 8 15 19 3jca φSalGenX=SSSAlgS=XXS
21 4 ad2antrr φSalGenX=SySAlgXyS=SalGenX
22 21 adantrl φSalGenX=SySAlgy=XXyS=SalGenX
23 11 ad2antrr φSalGenX=SySAlgXyXV
24 23 adantrl φSalGenX=SySAlgy=XXyXV
25 simplr φSalGenX=SySAlgXyySAlg
26 25 adantrl φSalGenX=SySAlgy=XXyySAlg
27 simpr φSalGenX=SySAlgXyXy
28 27 adantrl φSalGenX=SySAlgy=XXyXy
29 simprl φSalGenX=SySAlgy=XXyy=X
30 24 12 26 28 29 salgenss φSalGenX=SySAlgy=XXySalGenXy
31 22 30 eqsstrd φSalGenX=SySAlgy=XXySy
32 31 ex φSalGenX=SySAlgy=XXySy
33 32 ralrimiva φSalGenX=SySAlgy=XXySy
34 20 33 jca φSalGenX=SSSAlgS=XXSySAlgy=XXySy
35 34 ex φSalGenX=SSSAlgS=XXSySAlgy=XXySy
36 1 adantr φSSAlgS=XXSySAlgy=XXySyXV
37 simprl1 φSSAlgS=XXSySAlgy=XXySySSAlg
38 simprl2 φSSAlgS=XXSySAlgy=XXySyS=X
39 simprl3 φSSAlgS=XXSySAlgy=XXySyXS
40 unieq y=wy=w
41 40 eqeq1d y=wy=Xw=X
42 sseq2 y=wXyXw
43 41 42 anbi12d y=wy=XXyw=XXw
44 sseq2 y=wSySw
45 43 44 imbi12d y=wy=XXySyw=XXwSw
46 45 cbvralvw ySAlgy=XXySywSAlgw=XXwSw
47 46 biimpi ySAlgy=XXySywSAlgw=XXwSw
48 47 adantr ySAlgy=XXySywSAlgwSAlgw=XXwSw
49 simpr ySAlgy=XXySywSAlgwSAlg
50 48 49 jca ySAlgy=XXySywSAlgwSAlgw=XXwSwwSAlg
51 50 3ad2antr1 ySAlgy=XXySywSAlgw=XXwwSAlgw=XXwSwwSAlg
52 3simpc wSAlgw=XXww=XXw
53 52 adantl ySAlgy=XXySywSAlgw=XXww=XXw
54 rspa wSAlgw=XXwSwwSAlgw=XXwSw
55 51 53 54 sylc ySAlgy=XXySywSAlgw=XXwSw
56 55 adantll SSAlgS=XXSySAlgy=XXySywSAlgw=XXwSw
57 56 adantll φSSAlgS=XXSySAlgy=XXySywSAlgw=XXwSw
58 36 37 38 39 57 issalgend φSSAlgS=XXSySAlgy=XXySySalGenX=S
59 58 ex φSSAlgS=XXSySAlgy=XXySySalGenX=S
60 35 59 impbid φSalGenX=SSSAlgS=XXSySAlgy=XXySy