smfsup

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

Proof

Step	Hyp	Ref	Expression
1		smfsup.n	$⊢ \underline{Ⅎ} n F$
2		smfsup.x	$⊢ \underline{Ⅎ} x F$
3		smfsup.m	$⊢ φ \to M \in ℤ$
4		smfsup.z	$⊢ Z = ℤ_{\geq M}$
5		smfsup.s	$⊢ φ \to S \in SAlg$
6		smfsup.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smfsup.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
8		smfsup.g	$⊢ G = (x \in D ⟼ sup (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 F (n) (x) \leq y$
16		nfcv	$⊢ \underline{Ⅎ} x ℝ$
17		nfcv	$⊢ \underline{Ⅎ} x w$
18	12 17	nffv	$⊢ \underline{Ⅎ} x F (m) (w)$
19		nfcv	$⊢ \underline{Ⅎ} x \leq$
20		nfcv	$⊢ \underline{Ⅎ} x z$
21	18 19 20	nfbr	$⊢ Ⅎ x F (m) (w) \leq z$
22	10 21	nfralw	$⊢ Ⅎ x \forall m \in Z F (m) (w) \leq z$
23	16 22	nfrexw	$⊢ Ⅎ x \exists z \in ℝ \forall m \in Z F (m) (w) \leq z$
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	breq1d	$⊢ x = w \to (F (n) (x) \leq y \leftrightarrow F (n) (w) \leq y)$
34	33	ralbidv	$⊢ x = w \to (\forall n \in Z F (n) (x) \leq y \leftrightarrow \forall n \in Z F (n) (w) \leq y)$
35		nfv	$⊢ Ⅎ m F (n) (w) \leq y$
36		nfcv	$⊢ \underline{Ⅎ} n w$
37	26 36	nffv	$⊢ \underline{Ⅎ} n F (m) (w)$
38		nfcv	$⊢ \underline{Ⅎ} n \leq$
39		nfcv	$⊢ \underline{Ⅎ} n y$
40	37 38 39	nfbr	$⊢ Ⅎ n F (m) (w) \leq y$
41	28	fveq1d	$⊢ n = m \to F (n) (w) = F (m) (w)$
42	41	breq1d	$⊢ n = m \to (F (n) (w) \leq y \leftrightarrow F (m) (w) \leq y)$
43	35 40 42	cbvralw	$⊢ \forall n \in Z F (n) (w) \leq y \leftrightarrow \forall m \in Z F (m) (w) \leq y$
44	43	a1i	$⊢ x = w \to (\forall n \in Z F (n) (w) \leq y \leftrightarrow \forall m \in Z F (m) (w) \leq y)$
45	34 44	bitrd	$⊢ x = w \to (\forall n \in Z F (n) (x) \leq y \leftrightarrow \forall m \in Z F (m) (w) \leq y)$
46	45	rexbidv	$⊢ x = w \to (\exists y \in ℝ \forall n \in Z F (n) (x) \leq y \leftrightarrow \exists y \in ℝ \forall m \in Z F (m) (w) \leq y)$
47		breq2	$⊢ y = z \to (F (m) (w) \leq y \leftrightarrow F (m) (w) \leq z)$
48	47	ralbidv	$⊢ y = z \to (\forall m \in Z F (m) (w) \leq y \leftrightarrow \forall m \in Z F (m) (w) \leq z)$
49	48	cbvrexvw	$⊢ \exists y \in ℝ \forall m \in Z F (m) (w) \leq y \leftrightarrow \exists z \in ℝ \forall m \in Z F (m) (w) \leq z$
50	49	a1i	$⊢ x = w \to (\exists y \in ℝ \forall m \in Z F (m) (w) \leq y \leftrightarrow \exists z \in ℝ \forall m \in Z F (m) (w) \leq z)$
51	46 50	bitrd	$⊢ x = w \to (\exists y \in ℝ \forall n \in Z F (n) (x) \leq y \leftrightarrow \exists z \in ℝ \forall m \in Z F (m) (w) \leq z)$
52	9 14 15 23 31 51	cbvrabcsfw	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} = \{w \in ⋂_{m \in Z} dom F (m) \| \exists z \in ℝ \forall m \in Z F (m) (w) \leq z\}$
53	7 52	eqtri	$⊢ D = \{w \in ⋂_{m \in Z} dom F (m) \| \exists z \in ℝ \forall m \in Z F (m) (w) \leq z\}$
54		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
55	7 54	nfcxfr	$⊢ \underline{Ⅎ} x D$
56		nfcv	$⊢ \underline{Ⅎ} w D$
57		nfcv	$⊢ \underline{Ⅎ} w sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
58	10 18	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	nfsup	$⊢ \underline{Ⅎ} x sup (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 37 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	supeq1d	$⊢ x = w \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ <) = sup (ran (m \in Z ⟼ F (m) (w)) ℝ <)$
69	55 56 57 61 68	cbvmptf	$⊢ (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)) = (w \in D ⟼ sup (ran (m \in Z ⟼ F (m) (w)) ℝ <))$
70	8 69	eqtri	$⊢ G = (w \in D ⟼ sup (ran (m \in Z ⟼ F (m) (w)) ℝ <))$
71	3 4 5 6 53 70	smfsuplem3	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfsup

Proof