Metamath Proof Explorer

Theorem smfpimcc

Description: Given a countable set of sigma-measurable functions, and a Borel set A there exists a choice function h that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of A . This is a generalization of the observation at the beginning of the proof of Proposition 121F of Fremlin1 p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfpimcc.1 
|- F/_ n F
smfpimcc.z 
|- Z = ( ZZ>= ` M )
smfpimcc.s 
|- ( ph -> S e. SAlg )
smfpimcc.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfpimcc.j 
|- J = ( topGen ` ran (,) )
smfpimcc.b 
|- B = ( SalGen ` J )
smfpimcc.a 
|- ( ph -> A e. B )
Assertion smfpimcc 
|- ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )

Proof

Step Hyp Ref Expression
1 smfpimcc.1 
 |-  F/_ n F
2 smfpimcc.z 
 |-  Z = ( ZZ>= ` M )
3 smfpimcc.s 
 |-  ( ph -> S e. SAlg )
4 smfpimcc.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smfpimcc.j 
 |-  J = ( topGen ` ran (,) )
6 smfpimcc.b 
 |-  B = ( SalGen ` J )
7 smfpimcc.a 
 |-  ( ph -> A e. B )
8 2 uzct 
 |-  Z ~<_ _om
9 8 a1i 
 |-  ( ph -> Z ~<_ _om )
10 mptct 
 |-  ( Z ~<_ _om -> ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ~<_ _om )
11 rnct 
 |-  ( ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ~<_ _om -> ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ~<_ _om )
12 9 10 11 3syl 
 |-  ( ph -> ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ~<_ _om )
13 vex 
 |-  y e. _V
14 eqid 
 |-  ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) = ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
15 14 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) <-> E. m e. Z y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) )
16 13 15 ax-mp 
 |-  ( y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) <-> E. m e. Z y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
17 16 biimpi 
 |-  ( y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) -> E. m e. Z y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
18 17 adantl 
 |-  ( ( ph /\ y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ) -> E. m e. Z y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
19 simp3 
 |-  ( ( ph /\ m e. Z /\ y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) -> y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
20 3 adantr 
 |-  ( ( ph /\ m e. Z ) -> S e. SAlg )
21 4 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
22 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
23 7 adantr 
 |-  ( ( ph /\ m e. Z ) -> A e. B )
24 eqid 
 |-  ( `' ( F ` m ) " A ) = ( `' ( F ` m ) " A )
25 20 21 22 5 6 23 24 smfpimbor1 
 |-  ( ( ph /\ m e. Z ) -> ( `' ( F ` m ) " A ) e. ( S |`t dom ( F ` m ) ) )
26 fvex 
 |-  ( F ` m ) e. _V
27 26 dmex 
 |-  dom ( F ` m ) e. _V
28 27 a1i 
 |-  ( ph -> dom ( F ` m ) e. _V )
29 elrest 
 |-  ( ( S e. SAlg /\ dom ( F ` m ) e. _V ) -> ( ( `' ( F ` m ) " A ) e. ( S |`t dom ( F ` m ) ) <-> E. s e. S ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) ) )
30 3 28 29 syl2anc 
 |-  ( ph -> ( ( `' ( F ` m ) " A ) e. ( S |`t dom ( F ` m ) ) <-> E. s e. S ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) ) )
31 30 adantr 
 |-  ( ( ph /\ m e. Z ) -> ( ( `' ( F ` m ) " A ) e. ( S |`t dom ( F ` m ) ) <-> E. s e. S ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) ) )
32 25 31 mpbid 
 |-  ( ( ph /\ m e. Z ) -> E. s e. S ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) )
33 rabn0 
 |-  ( { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } =/= (/) <-> E. s e. S ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) )
34 32 33 sylibr 
 |-  ( ( ph /\ m e. Z ) -> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } =/= (/) )
35 34 3adant3 
 |-  ( ( ph /\ m e. Z /\ y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) -> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } =/= (/) )
36 19 35 eqnetrd 
 |-  ( ( ph /\ m e. Z /\ y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) -> y =/= (/) )
37 36 3exp 
 |-  ( ph -> ( m e. Z -> ( y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) ) )
38 37 rexlimdv 
 |-  ( ph -> ( E. m e. Z y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) )
39 38 adantr 
 |-  ( ( ph /\ y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ) -> ( E. m e. Z y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) )
40 18 39 mpd 
 |-  ( ( ph /\ y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ) -> y =/= (/) )
41 12 40 axccd2 
 |-  ( ph -> E. f A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y )
42 nfv 
 |-  F/ m ph
43 nfmpt1 
 |-  F/_ m ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
44 43 nfrn 
 |-  F/_ m ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
45 nfv 
 |-  F/ m ( f ` y ) e. y
46 44 45 nfralw 
 |-  F/ m A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y
47 42 46 nfan 
 |-  F/ m ( ph /\ A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y )
48 2 fvexi 
 |-  Z e. _V
49 3 adantr 
 |-  ( ( ph /\ A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y ) -> S e. SAlg )
50 fveq2 
 |-  ( y = w -> ( f ` y ) = ( f ` w ) )
51 id 
 |-  ( y = w -> y = w )
52 50 51 eleq12d 
 |-  ( y = w -> ( ( f ` y ) e. y <-> ( f ` w ) e. w ) )
53 52 rspccva 
 |-  ( ( A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y /\ w e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ) -> ( f ` w ) e. w )
54 53 adantll 
 |-  ( ( ( ph /\ A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y ) /\ w e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ) -> ( f ` w ) e. w )
55 eqid 
 |-  ( m e. Z |-> ( f ` { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ) = ( m e. Z |-> ( f ` { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) )
56 47 48 49 54 55 smfpimcclem 
 |-  ( ( ph /\ A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y ) -> E. h ( h : Z --> S /\ A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) )
57 56 ex 
 |-  ( ph -> ( A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y -> E. h ( h : Z --> S /\ A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) ) )
58 57 exlimdv 
 |-  ( ph -> ( E. f A. y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ( f ` y ) e. y -> E. h ( h : Z --> S /\ A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) ) )
59 41 58 mpd 
 |-  ( ph -> E. h ( h : Z --> S /\ A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) )
60 nfcv 
 |-  F/_ n m
61 1 60 nffv 
 |-  F/_ n ( F ` m )
62 61 nfcnv 
 |-  F/_ n `' ( F ` m )
63 nfcv 
 |-  F/_ n A
64 62 63 nfima 
 |-  F/_ n ( `' ( F ` m ) " A )
65 nfcv 
 |-  F/_ n ( h ` m )
66 61 nfdm 
 |-  F/_ n dom ( F ` m )
67 65 66 nfin 
 |-  F/_ n ( ( h ` m ) i^i dom ( F ` m ) )
68 64 67 nfeq 
 |-  F/ n ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) )
69 nfv 
 |-  F/ m ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) )
70 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
71 70 cnveqd 
 |-  ( m = n -> `' ( F ` m ) = `' ( F ` n ) )
72 71 imaeq1d 
 |-  ( m = n -> ( `' ( F ` m ) " A ) = ( `' ( F ` n ) " A ) )
73 fveq2 
 |-  ( m = n -> ( h ` m ) = ( h ` n ) )
74 70 dmeqd 
 |-  ( m = n -> dom ( F ` m ) = dom ( F ` n ) )
75 73 74 ineq12d 
 |-  ( m = n -> ( ( h ` m ) i^i dom ( F ` m ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) )
76 72 75 eqeq12d 
 |-  ( m = n -> ( ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) <-> ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )
77 68 69 76 cbvralw 
 |-  ( A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) <-> A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) )
78 77 anbi2i 
 |-  ( ( h : Z --> S /\ A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) <-> ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )
79 78 exbii 
 |-  ( E. h ( h : Z --> S /\ A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) <-> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )
80 59 79 sylib 
 |-  ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )