Metamath Proof Explorer

Theorem iunmbl2

Description: The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion iunmbl2 
|- ( ( A ~<_ NN /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol )

Proof

Step Hyp Ref Expression
1 brdom2 
 |-  ( A ~<_ NN <-> ( A ~< NN \/ A ~~ NN ) )
2 nnenom 
 |-  NN ~~ _om
3 sdomentr 
 |-  ( ( A ~< NN /\ NN ~~ _om ) -> A ~< _om )
4 2 3 mpan2 
 |-  ( A ~< NN -> A ~< _om )
5 isfinite 
 |-  ( A e. Fin <-> A ~< _om )
6 finiunmbl 
 |-  ( ( A e. Fin /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol )
7 6 ex 
 |-  ( A e. Fin -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
8 5 7 sylbir 
 |-  ( A ~< _om -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
9 4 8 syl 
 |-  ( A ~< NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
10 bren 
 |-  ( A ~~ NN <-> E. f f : A -1-1-onto-> NN )
11 nfv 
 |-  F/ n f : A -1-1-onto-> NN
12 nfcv 
 |-  F/_ n NN
13 nfcsb1v 
 |-  F/_ n [_ ( `' f ` k ) / n ]_ B
14 13 nfcri 
 |-  F/ n x e. [_ ( `' f ` k ) / n ]_ B
15 12 14 nfrexw 
 |-  F/ n E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B
16 f1of 
 |-  ( f : A -1-1-onto-> NN -> f : A --> NN )
17 16 ffvelcdmda 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A ) -> ( f ` n ) e. NN )
18 17 3adant3 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> ( f ` n ) e. NN )
19 simp3 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> x e. B )
20 f1ocnvfv1 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A ) -> ( `' f ` ( f ` n ) ) = n )
21 20 3adant3 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> ( `' f ` ( f ` n ) ) = n )
22 21 eqcomd 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> n = ( `' f ` ( f ` n ) ) )
23 csbeq1a 
 |-  ( n = ( `' f ` ( f ` n ) ) -> B = [_ ( `' f ` ( f ` n ) ) / n ]_ B )
24 22 23 syl 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> B = [_ ( `' f ` ( f ` n ) ) / n ]_ B )
25 19 24 eleqtrd 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> x e. [_ ( `' f ` ( f ` n ) ) / n ]_ B )
26 fveq2 
 |-  ( k = ( f ` n ) -> ( `' f ` k ) = ( `' f ` ( f ` n ) ) )
27 26 csbeq1d 
 |-  ( k = ( f ` n ) -> [_ ( `' f ` k ) / n ]_ B = [_ ( `' f ` ( f ` n ) ) / n ]_ B )
28 27 eleq2d 
 |-  ( k = ( f ` n ) -> ( x e. [_ ( `' f ` k ) / n ]_ B <-> x e. [_ ( `' f ` ( f ` n ) ) / n ]_ B ) )
29 28 rspcev 
 |-  ( ( ( f ` n ) e. NN /\ x e. [_ ( `' f ` ( f ` n ) ) / n ]_ B ) -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B )
30 18 25 29 syl2anc 
 |-  ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B )
31 30 3exp 
 |-  ( f : A -1-1-onto-> NN -> ( n e. A -> ( x e. B -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) ) )
32 11 15 31 rexlimd 
 |-  ( f : A -1-1-onto-> NN -> ( E. n e. A x e. B -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) )
33 f1ocnvdm 
 |-  ( ( f : A -1-1-onto-> NN /\ k e. NN ) -> ( `' f ` k ) e. A )
34 csbeq1a 
 |-  ( n = ( `' f ` k ) -> B = [_ ( `' f ` k ) / n ]_ B )
35 34 eleq2d 
 |-  ( n = ( `' f ` k ) -> ( x e. B <-> x e. [_ ( `' f ` k ) / n ]_ B ) )
36 14 35 rspce 
 |-  ( ( ( `' f ` k ) e. A /\ x e. [_ ( `' f ` k ) / n ]_ B ) -> E. n e. A x e. B )
37 36 ex 
 |-  ( ( `' f ` k ) e. A -> ( x e. [_ ( `' f ` k ) / n ]_ B -> E. n e. A x e. B ) )
38 33 37 syl 
 |-  ( ( f : A -1-1-onto-> NN /\ k e. NN ) -> ( x e. [_ ( `' f ` k ) / n ]_ B -> E. n e. A x e. B ) )
39 38 rexlimdva 
 |-  ( f : A -1-1-onto-> NN -> ( E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B -> E. n e. A x e. B ) )
40 32 39 impbid 
 |-  ( f : A -1-1-onto-> NN -> ( E. n e. A x e. B <-> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) )
41 eliun 
 |-  ( x e. U_ n e. A B <-> E. n e. A x e. B )
42 eliun 
 |-  ( x e. U_ k e. NN [_ ( `' f ` k ) / n ]_ B <-> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B )
43 40 41 42 3bitr4g 
 |-  ( f : A -1-1-onto-> NN -> ( x e. U_ n e. A B <-> x e. U_ k e. NN [_ ( `' f ` k ) / n ]_ B ) )
44 43 eqrdv 
 |-  ( f : A -1-1-onto-> NN -> U_ n e. A B = U_ k e. NN [_ ( `' f ` k ) / n ]_ B )
45 44 adantr 
 |-  ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> U_ n e. A B = U_ k e. NN [_ ( `' f ` k ) / n ]_ B )
46 rspcsbela 
 |-  ( ( ( `' f ` k ) e. A /\ A. n e. A B e. dom vol ) -> [_ ( `' f ` k ) / n ]_ B e. dom vol )
47 33 46 sylan 
 |-  ( ( ( f : A -1-1-onto-> NN /\ k e. NN ) /\ A. n e. A B e. dom vol ) -> [_ ( `' f ` k ) / n ]_ B e. dom vol )
48 47 an32s 
 |-  ( ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) /\ k e. NN ) -> [_ ( `' f ` k ) / n ]_ B e. dom vol )
49 48 ralrimiva 
 |-  ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> A. k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol )
50 iunmbl 
 |-  ( A. k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol -> U_ k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol )
51 49 50 syl 
 |-  ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> U_ k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol )
52 45 51 eqeltrd 
 |-  ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol )
53 52 ex 
 |-  ( f : A -1-1-onto-> NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
54 53 exlimiv 
 |-  ( E. f f : A -1-1-onto-> NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
55 10 54 sylbi 
 |-  ( A ~~ NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
56 9 55 jaoi 
 |-  ( ( A ~< NN \/ A ~~ NN ) -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
57 1 56 sylbi 
 |-  ( A ~<_ NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) )
58 57 imp 
 |-  ( ( A ~<_ NN /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol )