Metamath Proof Explorer

Theorem pwsal

Description: The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion pwsal 
|- ( X e. V -> ~P X e. SAlg )

Proof

Step Hyp Ref Expression
1 0elpw 
 |-  (/) e. ~P X
2 1 a1i 
 |-  ( X e. V -> (/) e. ~P X )
3 unipw 
 |-  U. ~P X = X
4 3 difeq1i 
 |-  ( U. ~P X \ y ) = ( X \ y )
5 4 a1i 
 |-  ( X e. V -> ( U. ~P X \ y ) = ( X \ y ) )
6 difssd 
 |-  ( X e. V -> ( X \ y ) C_ X )
7 difexg 
 |-  ( X e. V -> ( X \ y ) e. _V )
8 elpwg 
 |-  ( ( X \ y ) e. _V -> ( ( X \ y ) e. ~P X <-> ( X \ y ) C_ X ) )
9 7 8 syl 
 |-  ( X e. V -> ( ( X \ y ) e. ~P X <-> ( X \ y ) C_ X ) )
10 6 9 mpbird 
 |-  ( X e. V -> ( X \ y ) e. ~P X )
11 5 10 eqeltrd 
 |-  ( X e. V -> ( U. ~P X \ y ) e. ~P X )
12 11 adantr 
 |-  ( ( X e. V /\ y e. ~P X ) -> ( U. ~P X \ y ) e. ~P X )
13 12 ralrimiva 
 |-  ( X e. V -> A. y e. ~P X ( U. ~P X \ y ) e. ~P X )
14 elpwi 
 |-  ( y e. ~P ~P X -> y C_ ~P X )
15 14 unissd 
 |-  ( y e. ~P ~P X -> U. y C_ U. ~P X )
16 15 3 sseqtrdi 
 |-  ( y e. ~P ~P X -> U. y C_ X )
17 vuniex 
 |-  U. y e. _V
18 17 a1i 
 |-  ( y e. ~P ~P X -> U. y e. _V )
19 elpwg 
 |-  ( U. y e. _V -> ( U. y e. ~P X <-> U. y C_ X ) )
20 18 19 syl 
 |-  ( y e. ~P ~P X -> ( U. y e. ~P X <-> U. y C_ X ) )
21 16 20 mpbird 
 |-  ( y e. ~P ~P X -> U. y e. ~P X )
22 21 adantl 
 |-  ( ( X e. V /\ y e. ~P ~P X ) -> U. y e. ~P X )
23 22 a1d 
 |-  ( ( X e. V /\ y e. ~P ~P X ) -> ( y ~<_ _om -> U. y e. ~P X ) )
24 23 ralrimiva 
 |-  ( X e. V -> A. y e. ~P ~P X ( y ~<_ _om -> U. y e. ~P X ) )
25 2 13 24 3jca 
 |-  ( X e. V -> ( (/) e. ~P X /\ A. y e. ~P X ( U. ~P X \ y ) e. ~P X /\ A. y e. ~P ~P X ( y ~<_ _om -> U. y e. ~P X ) ) )
26 pwexg 
 |-  ( X e. V -> ~P X e. _V )
27 issal 
 |-  ( ~P X e. _V -> ( ~P X e. SAlg <-> ( (/) e. ~P X /\ A. y e. ~P X ( U. ~P X \ y ) e. ~P X /\ A. y e. ~P ~P X ( y ~<_ _om -> U. y e. ~P X ) ) ) )
28 26 27 syl 
 |-  ( X e. V -> ( ~P X e. SAlg <-> ( (/) e. ~P X /\ A. y e. ~P X ( U. ~P X \ y ) e. ~P X /\ A. y e. ~P ~P X ( y ~<_ _om -> U. y e. ~P X ) ) ) )
29 25 28 mpbird 
 |-  ( X e. V -> ~P X e. SAlg )