Metamath Proof Explorer

Theorem smfinfmpt

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

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

Proof

Step Hyp Ref Expression
1 smfinfmpt.n ⊢ Ⅎ n φ
2 smfinfmpt.x ⊢ Ⅎ x φ
3 smfinfmpt.y ⊢ Ⅎ y φ
4 smfinfmpt.m ⊢ φ → M ∈ ℤ
5 smfinfmpt.z ⊢ Z = ℤ ≥ M
6 smfinfmpt.s ⊢ φ → S ∈ SAlg
7 smfinfmpt.b ⊢ φ ∧ n ∈ Z ∧ x ∈ A → B ∈ V
8 smfinfmpt.f ⊢ φ ∧ n ∈ Z → x ∈ A ⟼ B ∈ SMblFn ⁡ S
9 smfinfmpt.d ⊢ D = x ∈ ⋂ n ∈ Z A | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B
10 smfinfmpt.g ⊢ G = x ∈ D ⟼ inf ran ⁡ 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 ⊢ Ⅎ _ x Z
15 14 nfcri ⊢ Ⅎ x n ∈ 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 ∈ Z A = ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
22 2 21 rabeqd ⊢ φ → x ∈ ⋂ n ∈ Z A | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B = x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B
23 nfv ⊢ Ⅎ y x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
24 3 23 nfan ⊢ Ⅎ y φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
25 nfii1 ⊢ Ⅎ _ n ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
26 25 nfcri ⊢ Ⅎ n x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
27 1 26 nfan ⊢ Ⅎ n φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
28 simpll ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ∧ n ∈ Z → φ
29 simpr ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ∧ n ∈ Z → n ∈ Z
30 eliinid ⊢ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ∧ n ∈ Z → x ∈ dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
31 30 adantll ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ∧ n ∈ Z → x ∈ dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n
32 13 19 eqtrd ⊢ φ ∧ n ∈ Z → dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n = A
33 32 adantlr ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ∧ n ∈ Z → dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n = A
34 31 33 eleqtrd ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ∧ n ∈ Z → x ∈ A
35 12 fveq1d ⊢ φ ∧ n ∈ Z → n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x = x ∈ A ⟼ B ⁡ x
36 35 3adant3 ⊢ φ ∧ n ∈ Z ∧ x ∈ A → n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x = x ∈ A ⟼ B ⁡ x
37 simp3 ⊢ φ ∧ n ∈ Z ∧ x ∈ A → x ∈ A
38 fvmpt4 ⊢ x ∈ A ∧ B ∈ V → x ∈ A ⟼ B ⁡ x = B
39 37 7 38 syl2anc ⊢ φ ∧ n ∈ Z ∧ x ∈ A → x ∈ A ⟼ B ⁡ x = B
40 36 39 eqtr2d ⊢ φ ∧ n ∈ Z ∧ x ∈ A → B = n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
41 40 breq2d ⊢ φ ∧ n ∈ Z ∧ x ∈ A → y ≤ B ↔ y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
42 28 29 34 41 syl3anc ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ∧ n ∈ Z → y ≤ B ↔ y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
43 27 42 ralbida ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n → ∀ n ∈ Z y ≤ B ↔ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
44 24 43 rexbid ⊢ φ ∧ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n → ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B ↔ ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
45 2 44 rabbida ⊢ φ → x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B = x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
46 22 45 eqtrd ⊢ φ → x ∈ ⋂ n ∈ Z A | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B = x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
47 9 46 eqtrid ⊢ φ → D = x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
48 nfcv ⊢ Ⅎ _ n ℝ
49 nfra1 ⊢ Ⅎ n ∀ n ∈ Z y ≤ B
50 48 49 nfrexw ⊢ Ⅎ n ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B
51 nfii1 ⊢ Ⅎ _ n ⋂ n ∈ Z A
52 50 51 nfrabw ⊢ Ⅎ _ n x ∈ ⋂ n ∈ Z A | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B
53 9 52 nfcxfr ⊢ Ⅎ _ n D
54 53 nfcri ⊢ Ⅎ n x ∈ D
55 1 54 nfan ⊢ Ⅎ n φ ∧ x ∈ D
56 simpll ⊢ φ ∧ x ∈ D ∧ n ∈ Z → φ
57 simpr ⊢ φ ∧ x ∈ D ∧ n ∈ Z → n ∈ Z
58 rabidim1 ⊢ x ∈ x ∈ ⋂ n ∈ Z A | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ B → x ∈ ⋂ n ∈ Z A
59 58 9 eleq2s ⊢ x ∈ D → x ∈ ⋂ n ∈ Z A
60 eliinid ⊢ x ∈ ⋂ n ∈ Z A ∧ n ∈ Z → x ∈ A
61 59 60 sylan ⊢ x ∈ D ∧ n ∈ Z → x ∈ A
62 61 adantll ⊢ φ ∧ x ∈ D ∧ n ∈ Z → x ∈ A
63 56 57 62 40 syl3anc ⊢ φ ∧ x ∈ D ∧ n ∈ Z → B = n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
64 55 63 mpteq2da ⊢ φ ∧ x ∈ D → n ∈ Z ⟼ B = n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
65 64 rneqd ⊢ φ ∧ x ∈ D → ran ⁡ n ∈ Z ⟼ B = ran ⁡ n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
66 65 infeq1d ⊢ φ ∧ x ∈ D → inf ran ⁡ n ∈ Z ⟼ B ℝ < = inf ran ⁡ n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ℝ <
67 2 47 66 mpteq12da ⊢ φ → x ∈ D ⟼ inf ran ⁡ n ∈ Z ⟼ B ℝ < = x ∈ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ⟼ inf ran ⁡ n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ℝ <
68 10 67 eqtrid ⊢ φ → G = x ∈ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ⟼ inf ran ⁡ n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ℝ <
69 nfmpt1 ⊢ Ⅎ _ n n ∈ Z ⟼ x ∈ A ⟼ B
70 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
71 14 70 nfmpt ⊢ Ⅎ _ x n ∈ Z ⟼ x ∈ A ⟼ B
72 1 8 fmptd2f ⊢ φ → n ∈ Z ⟼ x ∈ A ⟼ B : Z ⟶ SMblFn ⁡ S
73 eqid ⊢ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x = x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x
74 eqid ⊢ x ∈ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ⟼ inf ran ⁡ n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ℝ < = x ∈ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ⟼ inf ran ⁡ n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ℝ <
75 69 71 4 5 6 72 73 74 smfinf ⊢ φ → x ∈ x ∈ ⋂ n ∈ Z dom ⁡ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z y ≤ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ⟼ inf ran ⁡ n ∈ Z ⟼ n ∈ Z ⟼ x ∈ A ⟼ B ⁡ n ⁡ x ℝ < ∈ SMblFn ⁡ S
76 68 75 eqeltrd ⊢ φ → G ∈ SMblFn ⁡ S