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 bilani 
 |-  ( ( 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 ) ) } )
18 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 ) ) } )
19 3 adantr 
 |-  ( ( ph /\ m e. Z ) -> S e. SAlg )
20 4 ffvelcdmda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
21 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
22 7 adantr 
 |-  ( ( ph /\ m e. Z ) -> A e. B )
23 eqid 
 |-  ( `' ( F ` m ) " A ) = ( `' ( F ` m ) " A )
24 19 20 21 5 6 22 23 smfpimbor1 
 |-  ( ( ph /\ m e. Z ) -> ( `' ( F ` m ) " A ) e. ( S |`t dom ( F ` m ) ) )
25 fvex 
 |-  ( F ` m ) e. _V
26 25 dmex 
 |-  dom ( F ` m ) e. _V
27 26 a1i 
 |-  ( ph -> dom ( F ` m ) e. _V )
28 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 ) ) ) )
29 3 27 28 syl2anc 
 |-  ( ph -> ( ( `' ( F ` m ) " A ) e. ( S |`t dom ( F ` m ) ) <-> E. s e. S ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) ) )
30 29 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 ) ) ) )
31 24 30 mpbid 
 |-  ( ( ph /\ m e. Z ) -> E. s e. S ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) )
32 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 ) ) )
33 31 32 sylibr 
 |-  ( ( ph /\ m e. Z ) -> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } =/= (/) )
34 33 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 ) ) } =/= (/) )
35 18 34 eqnetrd 
 |-  ( ( ph /\ m e. Z /\ y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) -> y =/= (/) )
36 35 3exp 
 |-  ( ph -> ( m e. Z -> ( y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) ) )
37 36 rexlimdv 
 |-  ( ph -> ( E. m e. Z y = { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } -> y =/= (/) ) )
38 37 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 =/= (/) ) )
39 17 38 mpd 
 |-  ( ( ph /\ y e. ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } ) ) -> y =/= (/) )
40 12 39 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 )
41 nfv 
 |-  F/ m ph
42 nfmpt1 
 |-  F/_ m ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
43 42 nfrn 
 |-  F/_ m ran ( m e. Z |-> { s e. S | ( `' ( F ` m ) " A ) = ( s i^i dom ( F ` m ) ) } )
44 nfv 
 |-  F/ m ( f ` y ) e. y
45 43 44 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
46 41 45 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 )
47 2 fvexi 
 |-  Z e. _V
48 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 )
49 fveq2 
 |-  ( y = w -> ( f ` y ) = ( f ` w ) )
50 id 
 |-  ( y = w -> y = w )
51 49 50 eleq12d 
 |-  ( y = w -> ( ( f ` y ) e. y <-> ( f ` w ) e. w ) )
52 51 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 )
53 52 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 )
54 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 ) ) } ) )
55 46 47 48 53 54 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 ) ) ) )
56 55 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 ) ) ) ) )
57 56 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 ) ) ) ) )
58 40 57 mpd 
 |-  ( ph -> E. h ( h : Z --> S /\ A. m e. Z ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) ) )
59 nfcv 
 |-  F/_ n m
60 1 59 nffv 
 |-  F/_ n ( F ` m )
61 60 nfcnv 
 |-  F/_ n `' ( F ` m )
62 nfcv 
 |-  F/_ n A
63 61 62 nfima 
 |-  F/_ n ( `' ( F ` m ) " A )
64 nfcv 
 |-  F/_ n ( h ` m )
65 60 nfdm 
 |-  F/_ n dom ( F ` m )
66 64 65 nfin 
 |-  F/_ n ( ( h ` m ) i^i dom ( F ` m ) )
67 63 66 nfeq 
 |-  F/ n ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) )
68 nfv 
 |-  F/ m ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) )
69 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
70 69 cnveqd 
 |-  ( m = n -> `' ( F ` m ) = `' ( F ` n ) )
71 70 imaeq1d 
 |-  ( m = n -> ( `' ( F ` m ) " A ) = ( `' ( F ` n ) " A ) )
72 fveq2 
 |-  ( m = n -> ( h ` m ) = ( h ` n ) )
73 69 dmeqd 
 |-  ( m = n -> dom ( F ` m ) = dom ( F ` n ) )
74 72 73 ineq12d 
 |-  ( m = n -> ( ( h ` m ) i^i dom ( F ` m ) ) = ( ( h ` n ) i^i dom ( F ` n ) ) )
75 71 74 eqeq12d 
 |-  ( m = n -> ( ( `' ( F ` m ) " A ) = ( ( h ` m ) i^i dom ( F ` m ) ) <-> ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )
76 67 68 75 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 ) ) )
77 76 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 ) ) ) )
78 77 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 ) ) ) )
79 58 78 sylib 
 |-  ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )