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 _ n F
smfpimcc.z Z = M
smfpimcc.s φ S SAlg
smfpimcc.f φ F : Z SMblFn S
smfpimcc.j J = topGen ran .
smfpimcc.b B = SalGen J
smfpimcc.a φ A B
Assertion smfpimcc φ h h : Z S n Z F n -1 A = h n dom F n

Proof

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