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 nfrex
 |-  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 ffvelrnda
 |-  ( ( 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 )