Metamath Proof Explorer

Theorem saluncl

Description: The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion saluncl 
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E u. F ) e. S )

Proof

Step Hyp Ref Expression
1 uniprg 
 |-  ( ( E e. S /\ F e. S ) -> U. { E , F } = ( E u. F ) )
2 1 eqcomd 
 |-  ( ( E e. S /\ F e. S ) -> ( E u. F ) = U. { E , F } )
3 2 3adant1 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E u. F ) = U. { E , F } )
4 prfi 
 |-  { E , F } e. Fin
5 isfinite 
 |-  ( { E , F } e. Fin <-> { E , F } ~< _om )
6 5 biimpi 
 |-  ( { E , F } e. Fin -> { E , F } ~< _om )
7 sdomdom 
 |-  ( { E , F } ~< _om -> { E , F } ~<_ _om )
8 6 7 syl 
 |-  ( { E , F } e. Fin -> { E , F } ~<_ _om )
9 4 8 ax-mp 
 |-  { E , F } ~<_ _om
10 9 a1i 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> { E , F } ~<_ _om )
11 prelpwi 
 |-  ( ( E e. S /\ F e. S ) -> { E , F } e. ~P S )
12 11 3adant1 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> { E , F } e. ~P S )
13 issal 
 |-  ( S e. SAlg -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
14 13 ibi 
 |-  ( S e. SAlg -> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) )
15 14 simp3d 
 |-  ( S e. SAlg -> A. y e. ~P S ( y ~<_ _om -> U. y e. S ) )
16 15 3ad2ant1 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> A. y e. ~P S ( y ~<_ _om -> U. y e. S ) )
17 breq1 
 |-  ( y = { E , F } -> ( y ~<_ _om <-> { E , F } ~<_ _om ) )
18 unieq 
 |-  ( y = { E , F } -> U. y = U. { E , F } )
19 18 eleq1d 
 |-  ( y = { E , F } -> ( U. y e. S <-> U. { E , F } e. S ) )
20 17 19 imbi12d 
 |-  ( y = { E , F } -> ( ( y ~<_ _om -> U. y e. S ) <-> ( { E , F } ~<_ _om -> U. { E , F } e. S ) ) )
21 20 rspcva 
 |-  ( ( { E , F } e. ~P S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) -> ( { E , F } ~<_ _om -> U. { E , F } e. S ) )
22 12 16 21 syl2anc 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( { E , F } ~<_ _om -> U. { E , F } e. S ) )
23 10 22 mpd 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> U. { E , F } e. S )
24 3 23 eqeltrd 
 |-  ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E u. F ) e. S )