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 ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 iunxun ⊢ ∪ 𝑘 ∈ ( ( 1 ..^ 𝑁 ) ∪ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ( ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∪ ∪ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) )
2 fzossnn ⊢ ( 1 ..^ 𝑁 ) ⊆ ℕ
3 undif ⊢ ( ( 1 ..^ 𝑁 ) ⊆ ℕ ↔ ( ( 1 ..^ 𝑁 ) ∪ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ) = ℕ )
4 2 3 mpbi ⊢ ( ( 1 ..^ 𝑁 ) ∪ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ) = ℕ
5 iuneq1 ⊢ ( ( ( 1 ..^ 𝑁 ) ∪ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ) = ℕ → ∪ 𝑘 ∈ ( ( 1 ..^ 𝑁 ) ∪ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ∪ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) )
6 4 5 ax-mp ⊢ ∪ 𝑘 ∈ ( ( 1 ..^ 𝑁 ) ∪ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ∪ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ )
7 iftrue ⊢ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = 𝐴 )
8 7 iuneq2i ⊢ ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴
9 eldifn ⊢ ( 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) → ¬ 𝑘 ∈ ( 1 ..^ 𝑁 ) )
10 9 iffalsed ⊢ ( 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) → if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ∅ )
11 10 iuneq2i ⊢ ∪ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ∪ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ∅
12 iun0 ⊢ ∪ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) ∅ = ∅
13 11 12 eqtri ⊢ ∪ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ∅
14 8 13 uneq12i ⊢ ( ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∪ ∪ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑁 ) ) if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ) = ( ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∪ ∅ )
15 1 6 14 3eqtr3i ⊢ ∪ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ( ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∪ ∅ )
16 un0 ⊢ ( ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∪ ∅ ) = ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴
17 15 16 eqtri ⊢ ∪ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) = ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴
18 0elsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )
19 simpr ⊢ ( ( ( ( ∅ ∈ 𝑆 ∧ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → 𝐴 ∈ 𝑆 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) → 𝑘 ∈ ( 1 ..^ 𝑁 ) )
20 simpllr ⊢ ( ( ( ( ∅ ∈ 𝑆 ∧ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → 𝐴 ∈ 𝑆 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → 𝐴 ∈ 𝑆 ) )
21 19 20 mpd ⊢ ( ( ( ( ∅ ∈ 𝑆 ∧ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → 𝐴 ∈ 𝑆 ) ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) → 𝐴 ∈ 𝑆 )
22 simplll ⊢ ( ( ( ( ∅ ∈ 𝑆 ∧ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → 𝐴 ∈ 𝑆 ) ) ∧ 𝑘 ∈ ℕ ) ∧ ¬ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) → ∅ ∈ 𝑆 )
23 21 22 ifclda ⊢ ( ( ( ∅ ∈ 𝑆 ∧ ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → 𝐴 ∈ 𝑆 ) ) ∧ 𝑘 ∈ ℕ ) → if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 )
24 23 exp31 ⊢ ( ∅ ∈ 𝑆 → ( ( 𝑘 ∈ ( 1 ..^ 𝑁 ) → 𝐴 ∈ 𝑆 ) → ( 𝑘 ∈ ℕ → if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 ) ) )
25 24 ralimdv2 ⊢ ( ∅ ∈ 𝑆 → ( ∀ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 → ∀ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 ) )
26 25 imp ⊢ ( ( ∅ ∈ 𝑆 ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 ) → ∀ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 )
27 18 26 sylan ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 ) → ∀ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 )
28 sigaclcu2 ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 ) → ∪ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 )
29 27 28 syldan ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ℕ if ( 𝑘 ∈ ( 1 ..^ 𝑁 ) , 𝐴 , ∅ ) ∈ 𝑆 )
30 17 29 eqeltrrid ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐴 ∈ 𝑆 )