Metamath Proof Explorer

Theorem smfsupmpt

Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfsupmpt.n ⊢Ⅎnφ
smfsupmpt.x ⊢Ⅎxφ
smfsupmpt.y ⊢Ⅎyφ
smfsupmpt.m ⊢φ→M∈ℤ
smfsupmpt.z ⊢Z=ℤ≥M
smfsupmpt.s ⊢φ→S∈SAlg
smfsupmpt.b ⊢φ∧n∈Z∧x∈A→B∈V
smfsupmpt.f ⊢φ∧n∈Z→x∈A⟼B∈SMblFn⁡S
smfsupmpt.d ⊢D=x∈⋂n∈ZA|∃y∈ℝ∀n∈ZB≤y
smfsupmpt.g ⊢G=x∈D⟼supran⁡n∈Z⟼Bℝ<
Assertion smfsupmpt ⊢φ→G∈SMblFn⁡S

Proof

Step Hyp Ref Expression
1 smfsupmpt.n ⊢Ⅎnφ
2 smfsupmpt.x ⊢Ⅎxφ
3 smfsupmpt.y ⊢Ⅎyφ
4 smfsupmpt.m ⊢φ→M∈ℤ
5 smfsupmpt.z ⊢Z=ℤ≥M
6 smfsupmpt.s ⊢φ→S∈SAlg
7 smfsupmpt.b ⊢φ∧n∈Z∧x∈A→B∈V
8 smfsupmpt.f ⊢φ∧n∈Z→x∈A⟼B∈SMblFn⁡S
9 smfsupmpt.d ⊢D=x∈⋂n∈ZA|∃y∈ℝ∀n∈ZB≤y
10 smfsupmpt.g ⊢G=x∈D⟼supran⁡n∈Z⟼Bℝ<
11 eqidd ⊢φ→n∈Z⟼x∈A⟼B=n∈Z⟼x∈A⟼B
12 11 8 fvmpt2d ⊢φ∧n∈Z→n∈Z⟼x∈A⟼B⁡n=x∈A⟼B
13 12 dmeqd ⊢φ∧n∈Z→dom⁡n∈Z⟼x∈A⟼B⁡n=dom⁡x∈A⟼B
14 nfcv ⊢Ⅎ_xZ
15 14 nfcri ⊢Ⅎxn∈Z
16 2 15 nfan ⊢Ⅎxφ∧n∈Z
17 eqid ⊢x∈A⟼B=x∈A⟼B
18 7 3expa ⊢φ∧n∈Z∧x∈A→B∈V
19 16 17 18 dmmptdf ⊢φ∧n∈Z→dom⁡x∈A⟼B=A
20 13 19 eqtr2d ⊢φ∧n∈Z→A=dom⁡n∈Z⟼x∈A⟼B⁡n
21 1 20 iineq2d ⊢φ→⋂n∈ZA=⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n
22 nfcv ⊢Ⅎ_x⋂n∈ZA
23 nfmpt1 ⊢Ⅎ_xx∈A⟼B
24 14 23 nfmpt ⊢Ⅎ_xn∈Z⟼x∈A⟼B
25 nfcv ⊢Ⅎ_xn
26 24 25 nffv ⊢Ⅎ_xn∈Z⟼x∈A⟼B⁡n
27 26 nfdm ⊢Ⅎ_xdom⁡n∈Z⟼x∈A⟼B⁡n
28 14 27 nfiin ⊢Ⅎ_x⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n
29 22 28 rabeqf ⊢⋂n∈ZA=⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n→x∈⋂n∈ZA|∃y∈ℝ∀n∈ZB≤y=x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈ZB≤y
30 21 29 syl ⊢φ→x∈⋂n∈ZA|∃y∈ℝ∀n∈ZB≤y=x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈ZB≤y
31 nfv ⊢Ⅎyx∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n
32 3 31 nfan ⊢Ⅎyφ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n
33 nfii1 ⊢Ⅎ_n⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n
34 33 nfcri ⊢Ⅎnx∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n
35 1 34 nfan ⊢Ⅎnφ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n
36 simpll ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n∧n∈Z→φ
37 simpr ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n∧n∈Z→n∈Z
38 eliinid ⊢x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n∧n∈Z→x∈dom⁡n∈Z⟼x∈A⟼B⁡n
39 38 adantll ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n∧n∈Z→x∈dom⁡n∈Z⟼x∈A⟼B⁡n
40 13 19 eqtrd ⊢φ∧n∈Z→dom⁡n∈Z⟼x∈A⟼B⁡n=A
41 40 adantlr ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n∧n∈Z→dom⁡n∈Z⟼x∈A⟼B⁡n=A
42 39 41 eleqtrd ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n∧n∈Z→x∈A
43 12 fveq1d ⊢φ∧n∈Z→n∈Z⟼x∈A⟼B⁡n⁡x=x∈A⟼B⁡x
44 43 3adant3 ⊢φ∧n∈Z∧x∈A→n∈Z⟼x∈A⟼B⁡n⁡x=x∈A⟼B⁡x
45 simp3 ⊢φ∧n∈Z∧x∈A→x∈A
46 fvmpt4 ⊢x∈A∧B∈V→x∈A⟼B⁡x=B
47 45 7 46 syl2anc ⊢φ∧n∈Z∧x∈A→x∈A⟼B⁡x=B
48 44 47 eqtr2d ⊢φ∧n∈Z∧x∈A→B=n∈Z⟼x∈A⟼B⁡n⁡x
49 48 breq1d ⊢φ∧n∈Z∧x∈A→B≤y↔n∈Z⟼x∈A⟼B⁡n⁡x≤y
50 36 37 42 49 syl3anc ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n∧n∈Z→B≤y↔n∈Z⟼x∈A⟼B⁡n⁡x≤y
51 35 50 ralbida ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n→∀n∈ZB≤y↔∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y
52 32 51 rexbid ⊢φ∧x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n→∃y∈ℝ∀n∈ZB≤y↔∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y
53 2 52 rabbida ⊢φ→x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈ZB≤y=x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y
54 30 53 eqtrd ⊢φ→x∈⋂n∈ZA|∃y∈ℝ∀n∈ZB≤y=x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y
55 9 54 eqtrid ⊢φ→D=x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y
56 nfcv ⊢Ⅎ_nℝ
57 nfra1 ⊢Ⅎn∀n∈ZB≤y
58 56 57 nfrexw ⊢Ⅎn∃y∈ℝ∀n∈ZB≤y
59 nfii1 ⊢Ⅎ_n⋂n∈ZA
60 58 59 nfrabw ⊢Ⅎ_nx∈⋂n∈ZA|∃y∈ℝ∀n∈ZB≤y
61 9 60 nfcxfr ⊢Ⅎ_nD
62 61 nfcri ⊢Ⅎnx∈D
63 1 62 nfan ⊢Ⅎnφ∧x∈D
64 simpll ⊢φ∧x∈D∧n∈Z→φ
65 simpr ⊢φ∧x∈D∧n∈Z→n∈Z
66 rabidim1 ⊢x∈x∈⋂n∈ZA|∃y∈ℝ∀n∈ZB≤y→x∈⋂n∈ZA
67 66 9 eleq2s ⊢x∈D→x∈⋂n∈ZA
68 eliinid ⊢x∈⋂n∈ZA∧n∈Z→x∈A
69 67 68 sylan ⊢x∈D∧n∈Z→x∈A
70 69 adantll ⊢φ∧x∈D∧n∈Z→x∈A
71 64 65 70 48 syl3anc ⊢φ∧x∈D∧n∈Z→B=n∈Z⟼x∈A⟼B⁡n⁡x
72 63 71 mpteq2da ⊢φ∧x∈D→n∈Z⟼B=n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡x
73 72 rneqd ⊢φ∧x∈D→ran⁡n∈Z⟼B=ran⁡n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡x
74 73 supeq1d ⊢φ∧x∈D→supran⁡n∈Z⟼Bℝ<=supran⁡n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡xℝ<
75 2 55 74 mpteq12da ⊢φ→x∈D⟼supran⁡n∈Z⟼Bℝ<=x∈x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y⟼supran⁡n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡xℝ<
76 10 75 eqtrid ⊢φ→G=x∈x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y⟼supran⁡n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡xℝ<
77 nfmpt1 ⊢Ⅎ_nn∈Z⟼x∈A⟼B
78 1 8 fmptd2f ⊢φ→n∈Z⟼x∈A⟼B:Z⟶SMblFn⁡S
79 eqid ⊢x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y=x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y
80 eqid ⊢x∈x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y⟼supran⁡n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡xℝ<=x∈x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y⟼supran⁡n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡xℝ<
81 77 24 4 5 6 78 79 80 smfsup ⊢φ→x∈x∈⋂n∈Zdom⁡n∈Z⟼x∈A⟼B⁡n|∃y∈ℝ∀n∈Zn∈Z⟼x∈A⟼B⁡n⁡x≤y⟼supran⁡n∈Z⟼n∈Z⟼x∈A⟼B⁡n⁡xℝ<∈SMblFn⁡S
82 76 81 eqeltrd ⊢φ→G∈SMblFn⁡S