smfinf

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	smfinf.n	$⊢ \underline{Ⅎ} n F$
	smfinf.x	$⊢ \underline{Ⅎ} x F$
	smfinf.m	$⊢ φ \to M \in ℤ$
	smfinf.z	$⊢ Z = ℤ_{\geq M}$
	smfinf.s	$⊢ φ \to S \in SAlg$
	smfinf.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smfinf.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
	smfinf.g	$⊢ G = (x \in D ⟼ inf (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
Assertion	smfinf	$⊢ φ \to G \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfinf.n	$⊢ \underline{Ⅎ} n F$
2		smfinf.x	$⊢ \underline{Ⅎ} x F$
3		smfinf.m	$⊢ φ \to M \in ℤ$
4		smfinf.z	$⊢ Z = ℤ_{\geq M}$
5		smfinf.s	$⊢ φ \to S \in SAlg$
6		smfinf.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smfinf.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
8		smfinf.g	$⊢ G = (x \in D ⟼ inf (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
9		nfcv	$⊢ \underline{Ⅎ} w ⋂_{n \in Z} dom F (n)$
10		nfcv	$⊢ \underline{Ⅎ} x Z$
11		nfcv	$⊢ \underline{Ⅎ} x m$
12	2 11	nffv	$⊢ \underline{Ⅎ} x F (m)$
13	12	nfdm	$⊢ \underline{Ⅎ} x dom F (m)$
14	10 13	nfiin	$⊢ \underline{Ⅎ} x ⋂_{m \in Z} dom F (m)$
15		nfv	$⊢ Ⅎ w \exists y \in ℝ \forall n \in Z y \leq F (n) (x)$
16		nfcv	$⊢ \underline{Ⅎ} x ℝ$
17		nfcv	$⊢ \underline{Ⅎ} x z$
18		nfcv	$⊢ \underline{Ⅎ} x \leq$
19		nfcv	$⊢ \underline{Ⅎ} x w$
20	12 19	nffv	$⊢ \underline{Ⅎ} x F (m) (w)$
21	17 18 20	nfbr	$⊢ Ⅎ x z \leq F (m) (w)$
22	10 21	nfralw	$⊢ Ⅎ x \forall m \in Z z \leq F (m) (w)$
23	16 22	nfrexw	$⊢ Ⅎ x \exists z \in ℝ \forall m \in Z z \leq F (m) (w)$
24		nfcv	$⊢ \underline{Ⅎ} m dom F (n)$
25		nfcv	$⊢ \underline{Ⅎ} n m$
26	1 25	nffv	$⊢ \underline{Ⅎ} n F (m)$
27	26	nfdm	$⊢ \underline{Ⅎ} n dom F (m)$
28		fveq2	$⊢ n = m \to F (n) = F (m)$
29	28	dmeqd	$⊢ n = m \to dom F (n) = dom F (m)$
30	24 27 29	cbviin	$⊢ ⋂_{n \in Z} dom F (n) = ⋂_{m \in Z} dom F (m)$
31	30	a1i	$⊢ x = w \to ⋂_{n \in Z} dom F (n) = ⋂_{m \in Z} dom F (m)$
32		fveq2	$⊢ x = w \to F (n) (x) = F (n) (w)$
33	32	breq2d	$⊢ x = w \to (y \leq F (n) (x) \leftrightarrow y \leq F (n) (w))$
34	33	ralbidv	$⊢ x = w \to (\forall n \in Z y \leq F (n) (x) \leftrightarrow \forall n \in Z y \leq F (n) (w))$
35		nfv	$⊢ Ⅎ m y \leq F (n) (w)$
36		nfcv	$⊢ \underline{Ⅎ} n y$
37		nfcv	$⊢ \underline{Ⅎ} n \leq$
38		nfcv	$⊢ \underline{Ⅎ} n w$
39	26 38	nffv	$⊢ \underline{Ⅎ} n F (m) (w)$
40	36 37 39	nfbr	$⊢ Ⅎ n y \leq F (m) (w)$
41	28	fveq1d	$⊢ n = m \to F (n) (w) = F (m) (w)$
42	41	breq2d	$⊢ n = m \to (y \leq F (n) (w) \leftrightarrow y \leq F (m) (w))$
43	35 40 42	cbvralw	$⊢ \forall n \in Z y \leq F (n) (w) \leftrightarrow \forall m \in Z y \leq F (m) (w)$
44	43	a1i	$⊢ x = w \to (\forall n \in Z y \leq F (n) (w) \leftrightarrow \forall m \in Z y \leq F (m) (w))$
45	34 44	bitrd	$⊢ x = w \to (\forall n \in Z y \leq F (n) (x) \leftrightarrow \forall m \in Z y \leq F (m) (w))$
46	45	rexbidv	$⊢ x = w \to (\exists y \in ℝ \forall n \in Z y \leq F (n) (x) \leftrightarrow \exists y \in ℝ \forall m \in Z y \leq F (m) (w))$
47		breq1	$⊢ y = z \to (y \leq F (m) (w) \leftrightarrow z \leq F (m) (w))$
48	47	ralbidv	$⊢ y = z \to (\forall m \in Z y \leq F (m) (w) \leftrightarrow \forall m \in Z z \leq F (m) (w))$
49	48	cbvrexvw	$⊢ \exists y \in ℝ \forall m \in Z y \leq F (m) (w) \leftrightarrow \exists z \in ℝ \forall m \in Z z \leq F (m) (w)$
50	49	a1i	$⊢ x = w \to (\exists y \in ℝ \forall m \in Z y \leq F (m) (w) \leftrightarrow \exists z \in ℝ \forall m \in Z z \leq F (m) (w))$
51	46 50	bitrd	$⊢ x = w \to (\exists y \in ℝ \forall n \in Z y \leq F (n) (x) \leftrightarrow \exists z \in ℝ \forall m \in Z z \leq F (m) (w))$
52	9 14 15 23 31 51	cbvrabcsfw	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\} = \{w \in ⋂_{m \in Z} dom F (m) \| \exists z \in ℝ \forall m \in Z z \leq F (m) (w)\}$
53	7 52	eqtri	$⊢ D = \{w \in ⋂_{m \in Z} dom F (m) \| \exists z \in ℝ \forall m \in Z z \leq F (m) (w)\}$
54		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
55	7 54	nfcxfr	$⊢ \underline{Ⅎ} x D$
56		nfcv	$⊢ \underline{Ⅎ} w D$
57		nfcv	$⊢ \underline{Ⅎ} w inf (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
58	10 20	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ F (m) (w))$
59	58	nfrn	$⊢ \underline{Ⅎ} x ran (m \in Z ⟼ F (m) (w))$
60		nfcv	$⊢ \underline{Ⅎ} x <$
61	59 16 60	nfinf	$⊢ \underline{Ⅎ} x inf (ran (m \in Z ⟼ F (m) (w)) ℝ <)$
62	32	mpteq2dv	$⊢ x = w \to (n \in Z ⟼ F (n) (x)) = (n \in Z ⟼ F (n) (w))$
63		nfcv	$⊢ \underline{Ⅎ} m F (n) (w)$
64	63 39 41	cbvmpt	$⊢ (n \in Z ⟼ F (n) (w)) = (m \in Z ⟼ F (m) (w))$
65	64	a1i	$⊢ x = w \to (n \in Z ⟼ F (n) (w)) = (m \in Z ⟼ F (m) (w))$
66	62 65	eqtrd	$⊢ x = w \to (n \in Z ⟼ F (n) (x)) = (m \in Z ⟼ F (m) (w))$
67	66	rneqd	$⊢ x = w \to ran (n \in Z ⟼ F (n) (x)) = ran (m \in Z ⟼ F (m) (w))$
68	67	infeq1d	$⊢ x = w \to inf (ran (n \in Z ⟼ F (n) (x)) ℝ <) = inf (ran (m \in Z ⟼ F (m) (w)) ℝ <)$
69	55 56 57 61 68	cbvmptf	$⊢ (x \in D ⟼ inf (ran (n \in Z ⟼ F (n) (x)) ℝ <)) = (w \in D ⟼ inf (ran (m \in Z ⟼ F (m) (w)) ℝ <))$
70	8 69	eqtri	$⊢ G = (w \in D ⟼ inf (ran (m \in Z ⟼ F (m) (w)) ℝ <))$
71	3 4 5 6 53 70	smfinflem	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfinf

Proof