Metamath Proof Explorer

Theorem sigaclfu2

Description: A sigma-algebra is closed under finite union - indexing on ( 1 ..^ N ) . (Contributed by Thierry Arnoux, 28-Dec-2016)

Ref Expression
Assertion sigaclfu2 
|- ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ N ) A e. S ) -> U_ k e. ( 1 ..^ N ) A e. S )

Proof

Step Hyp Ref Expression
1 iunxun 
 |-  U_ k e. ( ( 1 ..^ N ) u. ( NN \ ( 1 ..^ N ) ) ) if ( k e. ( 1 ..^ N ) , A , (/) ) = ( U_ k e. ( 1 ..^ N ) if ( k e. ( 1 ..^ N ) , A , (/) ) u. U_ k e. ( NN \ ( 1 ..^ N ) ) if ( k e. ( 1 ..^ N ) , A , (/) ) )
2 fzossnn 
 |-  ( 1 ..^ N ) C_ NN
3 undif 
 |-  ( ( 1 ..^ N ) C_ NN <-> ( ( 1 ..^ N ) u. ( NN \ ( 1 ..^ N ) ) ) = NN )
4 2 3 mpbi 
 |-  ( ( 1 ..^ N ) u. ( NN \ ( 1 ..^ N ) ) ) = NN
5 iuneq1 
 |-  ( ( ( 1 ..^ N ) u. ( NN \ ( 1 ..^ N ) ) ) = NN -> U_ k e. ( ( 1 ..^ N ) u. ( NN \ ( 1 ..^ N ) ) ) if ( k e. ( 1 ..^ N ) , A , (/) ) = U_ k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) )
6 4 5 ax-mp 
 |-  U_ k e. ( ( 1 ..^ N ) u. ( NN \ ( 1 ..^ N ) ) ) if ( k e. ( 1 ..^ N ) , A , (/) ) = U_ k e. NN if ( k e. ( 1 ..^ N ) , A , (/) )
7 iftrue 
 |-  ( k e. ( 1 ..^ N ) -> if ( k e. ( 1 ..^ N ) , A , (/) ) = A )
8 7 iuneq2i 
 |-  U_ k e. ( 1 ..^ N ) if ( k e. ( 1 ..^ N ) , A , (/) ) = U_ k e. ( 1 ..^ N ) A
9 eldifn 
 |-  ( k e. ( NN \ ( 1 ..^ N ) ) -> -. k e. ( 1 ..^ N ) )
10 9 iffalsed 
 |-  ( k e. ( NN \ ( 1 ..^ N ) ) -> if ( k e. ( 1 ..^ N ) , A , (/) ) = (/) )
11 10 iuneq2i 
 |-  U_ k e. ( NN \ ( 1 ..^ N ) ) if ( k e. ( 1 ..^ N ) , A , (/) ) = U_ k e. ( NN \ ( 1 ..^ N ) ) (/)
12 iun0 
 |-  U_ k e. ( NN \ ( 1 ..^ N ) ) (/) = (/)
13 11 12 eqtri 
 |-  U_ k e. ( NN \ ( 1 ..^ N ) ) if ( k e. ( 1 ..^ N ) , A , (/) ) = (/)
14 8 13 uneq12i 
 |-  ( U_ k e. ( 1 ..^ N ) if ( k e. ( 1 ..^ N ) , A , (/) ) u. U_ k e. ( NN \ ( 1 ..^ N ) ) if ( k e. ( 1 ..^ N ) , A , (/) ) ) = ( U_ k e. ( 1 ..^ N ) A u. (/) )
15 1 6 14 3eqtr3i 
 |-  U_ k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) = ( U_ k e. ( 1 ..^ N ) A u. (/) )
16 un0 
 |-  ( U_ k e. ( 1 ..^ N ) A u. (/) ) = U_ k e. ( 1 ..^ N ) A
17 15 16 eqtri 
 |-  U_ k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) = U_ k e. ( 1 ..^ N ) A
18 0elsiga 
 |-  ( S e. U. ran sigAlgebra -> (/) e. S )
19 simpr 
 |-  ( ( ( ( (/) e. S /\ ( k e. ( 1 ..^ N ) -> A e. S ) ) /\ k e. NN ) /\ k e. ( 1 ..^ N ) ) -> k e. ( 1 ..^ N ) )
20 simpllr 
 |-  ( ( ( ( (/) e. S /\ ( k e. ( 1 ..^ N ) -> A e. S ) ) /\ k e. NN ) /\ k e. ( 1 ..^ N ) ) -> ( k e. ( 1 ..^ N ) -> A e. S ) )
21 19 20 mpd 
 |-  ( ( ( ( (/) e. S /\ ( k e. ( 1 ..^ N ) -> A e. S ) ) /\ k e. NN ) /\ k e. ( 1 ..^ N ) ) -> A e. S )
22 simplll 
 |-  ( ( ( ( (/) e. S /\ ( k e. ( 1 ..^ N ) -> A e. S ) ) /\ k e. NN ) /\ -. k e. ( 1 ..^ N ) ) -> (/) e. S )
23 21 22 ifclda 
 |-  ( ( ( (/) e. S /\ ( k e. ( 1 ..^ N ) -> A e. S ) ) /\ k e. NN ) -> if ( k e. ( 1 ..^ N ) , A , (/) ) e. S )
24 23 exp31 
 |-  ( (/) e. S -> ( ( k e. ( 1 ..^ N ) -> A e. S ) -> ( k e. NN -> if ( k e. ( 1 ..^ N ) , A , (/) ) e. S ) ) )
25 24 ralimdv2 
 |-  ( (/) e. S -> ( A. k e. ( 1 ..^ N ) A e. S -> A. k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) e. S ) )
26 25 imp 
 |-  ( ( (/) e. S /\ A. k e. ( 1 ..^ N ) A e. S ) -> A. k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) e. S )
27 18 26 sylan 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ N ) A e. S ) -> A. k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) e. S )
28 sigaclcu2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) e. S ) -> U_ k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) e. S )
29 27 28 syldan 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ N ) A e. S ) -> U_ k e. NN if ( k e. ( 1 ..^ N ) , A , (/) ) e. S )
30 17 29 eqeltrrid 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ N ) A e. S ) -> U_ k e. ( 1 ..^ N ) A e. S )