Metamath Proof Explorer

Theorem sigaclcu2

Description: A sigma-algebra is closed under countable union - indexing on NN (Contributed by Thierry Arnoux, 29-Dec-2016)

Ref Expression
Assertion sigaclcu2 
|- ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> U_ k e. NN A e. S )

Proof

Step Hyp Ref Expression
1 dfiun2g 
 |-  ( A. k e. NN A e. S -> U_ k e. NN A = U. { x | E. k e. NN x = A } )
2 1 adantl 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> U_ k e. NN A = U. { x | E. k e. NN x = A } )
3 simpl 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> S e. U. ran sigAlgebra )
4 abid 
 |-  ( x e. { x | E. k e. NN x = A } <-> E. k e. NN x = A )
5 eleq1a 
 |-  ( A e. S -> ( x = A -> x e. S ) )
6 5 ralimi 
 |-  ( A. k e. NN A e. S -> A. k e. NN ( x = A -> x e. S ) )
7 r19.23v 
 |-  ( A. k e. NN ( x = A -> x e. S ) <-> ( E. k e. NN x = A -> x e. S ) )
8 6 7 sylib 
 |-  ( A. k e. NN A e. S -> ( E. k e. NN x = A -> x e. S ) )
9 8 imp 
 |-  ( ( A. k e. NN A e. S /\ E. k e. NN x = A ) -> x e. S )
10 9 adantll 
 |-  ( ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) /\ E. k e. NN x = A ) -> x e. S )
11 4 10 sylan2b 
 |-  ( ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) /\ x e. { x | E. k e. NN x = A } ) -> x e. S )
12 11 ralrimiva 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> A. x e. { x | E. k e. NN x = A } x e. S )
13 nfab1 
 |-  F/_ x { x | E. k e. NN x = A }
14 nfcv 
 |-  F/_ x S
15 13 14 dfss3f 
 |-  ( { x | E. k e. NN x = A } C_ S <-> A. x e. { x | E. k e. NN x = A } x e. S )
16 12 15 sylibr 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> { x | E. k e. NN x = A } C_ S )
17 elpw2g 
 |-  ( S e. U. ran sigAlgebra -> ( { x | E. k e. NN x = A } e. ~P S <-> { x | E. k e. NN x = A } C_ S ) )
18 17 adantr 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> ( { x | E. k e. NN x = A } e. ~P S <-> { x | E. k e. NN x = A } C_ S ) )
19 16 18 mpbird 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> { x | E. k e. NN x = A } e. ~P S )
20 nnct 
 |-  NN ~<_ _om
21 abrexct 
 |-  ( NN ~<_ _om -> { x | E. k e. NN x = A } ~<_ _om )
22 20 21 mp1i 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> { x | E. k e. NN x = A } ~<_ _om )
23 sigaclcu 
 |-  ( ( S e. U. ran sigAlgebra /\ { x | E. k e. NN x = A } e. ~P S /\ { x | E. k e. NN x = A } ~<_ _om ) -> U. { x | E. k e. NN x = A } e. S )
24 3 19 22 23 syl3anc 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> U. { x | E. k e. NN x = A } e. S )
25 2 24 eqeltrd 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> U_ k e. NN A e. S )