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 
|- ( ph -> X e. V )
Assertion dfsalgen2 
|- ( ph -> ( ( SalGen ` X ) = S <-> ( ( S e. SAlg /\ U. S = U. X /\ X C_ S ) /\ A. y e. SAlg ( ( U. y = U. X /\ X C_ y ) -> S C_ y ) ) ) )

Proof

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