Metamath Proof Explorer

Theorem prsal

Description: The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion prsal 
|- ( X e. V -> { (/) , X } e. SAlg )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 prid1 
 |-  (/) e. { (/) , X }
3 2 a1i 
 |-  ( X e. V -> (/) e. { (/) , X } )
4 uniprg 
 |-  ( ( (/) e. _V /\ X e. V ) -> U. { (/) , X } = ( (/) u. X ) )
5 1 4 mpan 
 |-  ( X e. V -> U. { (/) , X } = ( (/) u. X ) )
6 0un 
 |-  ( (/) u. X ) = X
7 5 6 eqtrdi 
 |-  ( X e. V -> U. { (/) , X } = X )
8 7 difeq1d 
 |-  ( X e. V -> ( U. { (/) , X } \ y ) = ( X \ y ) )
9 8 adantr 
 |-  ( ( X e. V /\ y e. { (/) , X } ) -> ( U. { (/) , X } \ y ) = ( X \ y ) )
10 difeq2 
 |-  ( y = (/) -> ( X \ y ) = ( X \ (/) ) )
11 10 adantl 
 |-  ( ( X e. V /\ y = (/) ) -> ( X \ y ) = ( X \ (/) ) )
12 dif0 
 |-  ( X \ (/) ) = X
13 11 12 eqtrdi 
 |-  ( ( X e. V /\ y = (/) ) -> ( X \ y ) = X )
14 prid2g 
 |-  ( X e. V -> X e. { (/) , X } )
15 14 adantr 
 |-  ( ( X e. V /\ y = (/) ) -> X e. { (/) , X } )
16 13 15 eqeltrd 
 |-  ( ( X e. V /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
17 16 adantlr 
 |-  ( ( ( X e. V /\ y e. { (/) , X } ) /\ y = (/) ) -> ( X \ y ) e. { (/) , X } )
18 neqne 
 |-  ( -. y = (/) -> y =/= (/) )
19 elprn1 
 |-  ( ( y e. { (/) , X } /\ y =/= (/) ) -> y = X )
20 18 19 sylan2 
 |-  ( ( y e. { (/) , X } /\ -. y = (/) ) -> y = X )
21 20 adantll 
 |-  ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> y = X )
22 difeq2 
 |-  ( y = X -> ( X \ y ) = ( X \ X ) )
23 difid 
 |-  ( X \ X ) = (/)
24 22 23 eqtrdi 
 |-  ( y = X -> ( X \ y ) = (/) )
25 2 a1i 
 |-  ( y = X -> (/) e. { (/) , X } )
26 24 25 eqeltrd 
 |-  ( y = X -> ( X \ y ) e. { (/) , X } )
27 21 26 syl 
 |-  ( ( ( X e. V /\ y e. { (/) , X } ) /\ -. y = (/) ) -> ( X \ y ) e. { (/) , X } )
28 17 27 pm2.61dan 
 |-  ( ( X e. V /\ y e. { (/) , X } ) -> ( X \ y ) e. { (/) , X } )
29 9 28 eqeltrd 
 |-  ( ( X e. V /\ y e. { (/) , X } ) -> ( U. { (/) , X } \ y ) e. { (/) , X } )
30 29 ralrimiva 
 |-  ( X e. V -> A. y e. { (/) , X } ( U. { (/) , X } \ y ) e. { (/) , X } )
31 elpwi 
 |-  ( y e. ~P { (/) , X } -> y C_ { (/) , X } )
32 31 unissd 
 |-  ( y e. ~P { (/) , X } -> U. y C_ U. { (/) , X } )
33 32 adantl 
 |-  ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y C_ U. { (/) , X } )
34 7 adantr 
 |-  ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. { (/) , X } = X )
35 33 34 sseqtrd 
 |-  ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y C_ X )
36 35 adantr 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y C_ X )
37 elssuni 
 |-  ( X e. y -> X C_ U. y )
38 37 adantl 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> X C_ U. y )
39 36 38 eqssd 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y = X )
40 14 ad2antrr 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> X e. { (/) , X } )
41 39 40 eqeltrd 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ X e. y ) -> U. y e. { (/) , X } )
42 id 
 |-  ( y e. ~P { (/) , X } -> y e. ~P { (/) , X } )
43 pwpr 
 |-  ~P { (/) , X } = ( { (/) , { (/) } } u. { { X } , { (/) , X } } )
44 42 43 eleqtrdi 
 |-  ( y e. ~P { (/) , X } -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
45 44 adantr 
 |-  ( ( y e. ~P { (/) , X } /\ -. X e. y ) -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
46 45 adantll 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) )
47 snidg 
 |-  ( X e. V -> X e. { X } )
48 47 adantr 
 |-  ( ( X e. V /\ y = { X } ) -> X e. { X } )
49 id 
 |-  ( y = { X } -> y = { X } )
50 49 eqcomd 
 |-  ( y = { X } -> { X } = y )
51 50 adantl 
 |-  ( ( X e. V /\ y = { X } ) -> { X } = y )
52 48 51 eleqtrd 
 |-  ( ( X e. V /\ y = { X } ) -> X e. y )
53 52 adantlr 
 |-  ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ y = { X } ) -> X e. y )
54 id 
 |-  ( X e. V -> X e. V )
55 54 ad2antrr 
 |-  ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> X e. V )
56 neqne 
 |-  ( -. y = { X } -> y =/= { X } )
57 elprn1 
 |-  ( ( y e. { { X } , { (/) , X } } /\ y =/= { X } ) -> y = { (/) , X } )
58 56 57 sylan2 
 |-  ( ( y e. { { X } , { (/) , X } } /\ -. y = { X } ) -> y = { (/) , X } )
59 58 adantll 
 |-  ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> y = { (/) , X } )
60 14 adantr 
 |-  ( ( X e. V /\ y = { (/) , X } ) -> X e. { (/) , X } )
61 id 
 |-  ( y = { (/) , X } -> y = { (/) , X } )
62 61 eqcomd 
 |-  ( y = { (/) , X } -> { (/) , X } = y )
63 62 adantl 
 |-  ( ( X e. V /\ y = { (/) , X } ) -> { (/) , X } = y )
64 60 63 eleqtrd 
 |-  ( ( X e. V /\ y = { (/) , X } ) -> X e. y )
65 55 59 64 syl2anc 
 |-  ( ( ( X e. V /\ y e. { { X } , { (/) , X } } ) /\ -. y = { X } ) -> X e. y )
66 53 65 pm2.61dan 
 |-  ( ( X e. V /\ y e. { { X } , { (/) , X } } ) -> X e. y )
67 66 stoic1a 
 |-  ( ( X e. V /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
68 67 adantlr 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> -. y e. { { X } , { (/) , X } } )
69 elunnel2 
 |-  ( ( y e. ( { (/) , { (/) } } u. { { X } , { (/) , X } } ) /\ -. y e. { { X } , { (/) , X } } ) -> y e. { (/) , { (/) } } )
70 46 68 69 syl2anc 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> y e. { (/) , { (/) } } )
71 unieq 
 |-  ( y = (/) -> U. y = U. (/) )
72 uni0 
 |-  U. (/) = (/)
73 71 72 eqtrdi 
 |-  ( y = (/) -> U. y = (/) )
74 73 adantl 
 |-  ( ( y e. { (/) , { (/) } } /\ y = (/) ) -> U. y = (/) )
75 elprn1 
 |-  ( ( y e. { (/) , { (/) } } /\ y =/= (/) ) -> y = { (/) } )
76 18 75 sylan2 
 |-  ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> y = { (/) } )
77 unieq 
 |-  ( y = { (/) } -> U. y = U. { (/) } )
78 unisn0 
 |-  U. { (/) } = (/)
79 77 78 eqtrdi 
 |-  ( y = { (/) } -> U. y = (/) )
80 76 79 syl 
 |-  ( ( y e. { (/) , { (/) } } /\ -. y = (/) ) -> U. y = (/) )
81 74 80 pm2.61dan 
 |-  ( y e. { (/) , { (/) } } -> U. y = (/) )
82 70 81 syl 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> U. y = (/) )
83 2 a1i 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> (/) e. { (/) , X } )
84 82 83 eqeltrd 
 |-  ( ( ( X e. V /\ y e. ~P { (/) , X } ) /\ -. X e. y ) -> U. y e. { (/) , X } )
85 41 84 pm2.61dan 
 |-  ( ( X e. V /\ y e. ~P { (/) , X } ) -> U. y e. { (/) , X } )
86 85 a1d 
 |-  ( ( X e. V /\ y e. ~P { (/) , X } ) -> ( y ~<_ _om -> U. y e. { (/) , X } ) )
87 86 ralrimiva 
 |-  ( X e. V -> A. y e. ~P { (/) , X } ( y ~<_ _om -> U. y e. { (/) , X } ) )
88 prex 
 |-  { (/) , X } e. _V
89 issal 
 |-  ( { (/) , X } e. _V -> ( { (/) , X } e. SAlg <-> ( (/) e. { (/) , X } /\ A. y e. { (/) , X } ( U. { (/) , X } \ y ) e. { (/) , X } /\ A. y e. ~P { (/) , X } ( y ~<_ _om -> U. y e. { (/) , X } ) ) ) )
90 88 89 mp1i 
 |-  ( X e. V -> ( { (/) , X } e. SAlg <-> ( (/) e. { (/) , X } /\ A. y e. { (/) , X } ( U. { (/) , X } \ y ) e. { (/) , X } /\ A. y e. ~P { (/) , X } ( y ~<_ _om -> U. y e. { (/) , X } ) ) ) )
91 3 30 87 90 mpbir3and 
 |-  ( X e. V -> { (/) , X } e. SAlg )