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 𝑛 𝐹
smfpimcc.z 𝑍 = ( ℤ𝑀 )
smfpimcc.s ( 𝜑𝑆 ∈ SAlg )
smfpimcc.f ( 𝜑𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smfpimcc.j 𝐽 = ( topGen ‘ ran (,) )
smfpimcc.b 𝐵 = ( SalGen ‘ 𝐽 )
smfpimcc.a ( 𝜑𝐴𝐵 )
Assertion smfpimcc ( 𝜑 → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 smfpimcc.1 𝑛 𝐹
2 smfpimcc.z 𝑍 = ( ℤ𝑀 )
3 smfpimcc.s ( 𝜑𝑆 ∈ SAlg )
4 smfpimcc.f ( 𝜑𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smfpimcc.j 𝐽 = ( topGen ‘ ran (,) )
6 smfpimcc.b 𝐵 = ( SalGen ‘ 𝐽 )
7 smfpimcc.a ( 𝜑𝐴𝐵 )
8 2 uzct 𝑍 ≼ ω
9 8 a1i ( 𝜑𝑍 ≼ ω )
10 mptct ( 𝑍 ≼ ω → ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ≼ ω )
11 rnct ( ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ≼ ω → ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ≼ ω )
12 9 10 11 3syl ( 𝜑 → ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ≼ ω )
13 vex 𝑦 ∈ V
14 eqid ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) = ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
15 14 elrnmpt ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ↔ ∃ 𝑚𝑍 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) )
16 13 15 ax-mp ( 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ↔ ∃ 𝑚𝑍 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
17 16 biimpi ( 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) → ∃ 𝑚𝑍 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
18 17 adantl ( ( 𝜑𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ) → ∃ 𝑚𝑍 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
19 simp3 ( ( 𝜑𝑚𝑍𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) → 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
20 3 adantr ( ( 𝜑𝑚𝑍 ) → 𝑆 ∈ SAlg )
21 4 ffvelrnda ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
22 eqid dom ( 𝐹𝑚 ) = dom ( 𝐹𝑚 )
23 7 adantr ( ( 𝜑𝑚𝑍 ) → 𝐴𝐵 )
24 eqid ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝐹𝑚 ) “ 𝐴 )
25 20 21 22 5 6 23 24 smfpimbor1 ( ( 𝜑𝑚𝑍 ) → ( ( 𝐹𝑚 ) “ 𝐴 ) ∈ ( 𝑆t dom ( 𝐹𝑚 ) ) )
26 fvex ( 𝐹𝑚 ) ∈ V
27 26 dmex dom ( 𝐹𝑚 ) ∈ V
28 27 a1i ( 𝜑 → dom ( 𝐹𝑚 ) ∈ V )
29 elrest ( ( 𝑆 ∈ SAlg ∧ dom ( 𝐹𝑚 ) ∈ V ) → ( ( ( 𝐹𝑚 ) “ 𝐴 ) ∈ ( 𝑆t dom ( 𝐹𝑚 ) ) ↔ ∃ 𝑠𝑆 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) ) )
30 3 28 29 syl2anc ( 𝜑 → ( ( ( 𝐹𝑚 ) “ 𝐴 ) ∈ ( 𝑆t dom ( 𝐹𝑚 ) ) ↔ ∃ 𝑠𝑆 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) ) )
31 30 adantr ( ( 𝜑𝑚𝑍 ) → ( ( ( 𝐹𝑚 ) “ 𝐴 ) ∈ ( 𝑆t dom ( 𝐹𝑚 ) ) ↔ ∃ 𝑠𝑆 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) ) )
32 25 31 mpbid ( ( 𝜑𝑚𝑍 ) → ∃ 𝑠𝑆 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) )
33 rabn0 ( { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ≠ ∅ ↔ ∃ 𝑠𝑆 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) )
34 32 33 sylibr ( ( 𝜑𝑚𝑍 ) → { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ≠ ∅ )
35 34 3adant3 ( ( 𝜑𝑚𝑍𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) → { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ≠ ∅ )
36 19 35 eqnetrd ( ( 𝜑𝑚𝑍𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) → 𝑦 ≠ ∅ )
37 36 3exp ( 𝜑 → ( 𝑚𝑍 → ( 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } → 𝑦 ≠ ∅ ) ) )
38 37 rexlimdv ( 𝜑 → ( ∃ 𝑚𝑍 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } → 𝑦 ≠ ∅ ) )
39 38 adantr ( ( 𝜑𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ) → ( ∃ 𝑚𝑍 𝑦 = { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } → 𝑦 ≠ ∅ ) )
40 18 39 mpd ( ( 𝜑𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ) → 𝑦 ≠ ∅ )
41 12 40 axccd2 ( 𝜑 → ∃ 𝑓𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦 )
42 nfv 𝑚 𝜑
43 nfmpt1 𝑚 ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
44 43 nfrn 𝑚 ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } )
45 nfv 𝑚 ( 𝑓𝑦 ) ∈ 𝑦
46 44 45 nfralw 𝑚𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦
47 42 46 nfan 𝑚 ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦 )
48 2 fvexi 𝑍 ∈ V
49 3 adantr ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦 ) → 𝑆 ∈ SAlg )
50 fveq2 ( 𝑦 = 𝑤 → ( 𝑓𝑦 ) = ( 𝑓𝑤 ) )
51 id ( 𝑦 = 𝑤𝑦 = 𝑤 )
52 50 51 eleq12d ( 𝑦 = 𝑤 → ( ( 𝑓𝑦 ) ∈ 𝑦 ↔ ( 𝑓𝑤 ) ∈ 𝑤 ) )
53 52 rspccva ( ( ∀ 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦𝑤 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ) → ( 𝑓𝑤 ) ∈ 𝑤 )
54 53 adantll ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦 ) ∧ 𝑤 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ) → ( 𝑓𝑤 ) ∈ 𝑤 )
55 eqid ( 𝑚𝑍 ↦ ( 𝑓 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ) = ( 𝑚𝑍 ↦ ( 𝑓 ‘ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) )
56 47 48 49 54 55 smfpimcclem ( ( 𝜑 ∧ ∀ 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦 ) → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑚𝑍 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ) )
57 56 ex ( 𝜑 → ( ∀ 𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦 → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑚𝑍 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ) ) )
58 57 exlimdv ( 𝜑 → ( ∃ 𝑓𝑦 ∈ ran ( 𝑚𝑍 ↦ { 𝑠𝑆 ∣ ( ( 𝐹𝑚 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹𝑚 ) ) } ) ( 𝑓𝑦 ) ∈ 𝑦 → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑚𝑍 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ) ) )
59 41 58 mpd ( 𝜑 → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑚𝑍 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ) )
60 nfcv 𝑛 𝑚
61 1 60 nffv 𝑛 ( 𝐹𝑚 )
62 61 nfcnv 𝑛 ( 𝐹𝑚 )
63 nfcv 𝑛 𝐴
64 62 63 nfima 𝑛 ( ( 𝐹𝑚 ) “ 𝐴 )
65 nfcv 𝑛 ( 𝑚 )
66 61 nfdm 𝑛 dom ( 𝐹𝑚 )
67 65 66 nfin 𝑛 ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) )
68 64 67 nfeq 𝑛 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) )
69 nfv 𝑚 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) )
70 fveq2 ( 𝑚 = 𝑛 → ( 𝐹𝑚 ) = ( 𝐹𝑛 ) )
71 70 cnveqd ( 𝑚 = 𝑛 ( 𝐹𝑚 ) = ( 𝐹𝑛 ) )
72 71 imaeq1d ( 𝑚 = 𝑛 → ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝐹𝑛 ) “ 𝐴 ) )
73 fveq2 ( 𝑚 = 𝑛 → ( 𝑚 ) = ( 𝑛 ) )
74 70 dmeqd ( 𝑚 = 𝑛 → dom ( 𝐹𝑚 ) = dom ( 𝐹𝑛 ) )
75 73 74 ineq12d ( 𝑚 = 𝑛 → ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) )
76 72 75 eqeq12d ( 𝑚 = 𝑛 → ( ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ↔ ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )
77 68 69 76 cbvralw ( ∀ 𝑚𝑍 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ↔ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) )
78 77 anbi2i ( ( : 𝑍𝑆 ∧ ∀ 𝑚𝑍 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ) ↔ ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )
79 78 exbii ( ∃ ( : 𝑍𝑆 ∧ ∀ 𝑚𝑍 ( ( 𝐹𝑚 ) “ 𝐴 ) = ( ( 𝑚 ) ∩ dom ( 𝐹𝑚 ) ) ) ↔ ∃ ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )
80 59 79 sylib ( 𝜑 → ∃ ( : 𝑍𝑆 ∧ ∀ 𝑛𝑍 ( ( 𝐹𝑛 ) “ 𝐴 ) = ( ( 𝑛 ) ∩ dom ( 𝐹𝑛 ) ) ) )