smfsupxr

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

Proof

Step	Hyp	Ref	Expression
1		smfsupxr.n	$⊢ \underline{Ⅎ} n F$
2		smfsupxr.x	$⊢ \underline{Ⅎ} x F$
3		smfsupxr.m	$⊢ φ \to M \in ℤ$
4		smfsupxr.z	$⊢ Z = ℤ_{\geq M}$
5		smfsupxr.s	$⊢ φ \to S \in SAlg$
6		smfsupxr.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smfsupxr.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ\}$
8		smfsupxr.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <))$
9	8	a1i	$⊢ φ \to G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <))$
10	7	a1i	$⊢ φ \to D = \{x \in ⋂_{n \in Z} dom F (n) \| sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ\}$
11		nfv	$⊢ Ⅎ n φ$
12		nfcv	$⊢ \underline{Ⅎ} n x$
13		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} dom F (n)$
14	12 13	nfel	$⊢ Ⅎ n x \in ⋂_{n \in Z} dom F (n)$
15	11 14	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in Z} dom F (n))$
16	3 4	uzn0d	$⊢ φ \to Z \neq \emptyset$
17	16	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to Z \neq \emptyset$
18	5	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
19	6	ffvelrnda	$⊢ (φ \land n \in Z) \to F (n) \in SMblFn (S)$
20		eqid	$⊢ dom F (n) = dom F (n)$
21	18 19 20	smff	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
22	21	adantlr	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
23		eliinid	$⊢ (x \in ⋂_{n \in Z} dom F (n) \land n \in Z) \to x \in dom F (n)$
24	23	adantll	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land n \in Z) \to x \in dom F (n)$
25	22 24	ffvelrnd	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land n \in Z) \to F (n) (x) \in ℝ$
26	15 17 25	supxrre3rnmpt	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to (sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ \leftrightarrow \exists y \in ℝ \forall n \in Z F (n) (x) \leq y)$
27	26	rabbidva	$⊢ φ \to \{x \in ⋂_{n \in Z} dom F (n) \| sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ\} = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
28	10 27	eqtrd	$⊢ φ \to D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
29		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ F (n) (x))$
30	29	nfrn	$⊢ \underline{Ⅎ} n ran (n \in Z ⟼ F (n) (x))$
31		nfcv	$⊢ \underline{Ⅎ} n ℝ^{*}$
32		nfcv	$⊢ \underline{Ⅎ} n <$
33	30 31 32	nfsup	$⊢ \underline{Ⅎ} n sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <)$
34		nfcv	$⊢ \underline{Ⅎ} n ℝ$
35	33 34	nfel	$⊢ Ⅎ n sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ$
36	35 13	nfrabw	$⊢ \underline{Ⅎ} n \{x \in ⋂_{n \in Z} dom F (n) \| sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ\}$
37	7 36	nfcxfr	$⊢ \underline{Ⅎ} n D$
38	12 37	nfel	$⊢ Ⅎ n x \in D$
39	11 38	nfan	$⊢ Ⅎ n (φ \land x \in D)$
40	16	adantr	$⊢ (φ \land x \in D) \to Z \neq \emptyset$
41	21	adantlr	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
42		nfcv	$⊢ \underline{Ⅎ} x Z$
43		nfcv	$⊢ \underline{Ⅎ} x n$
44	2 43	nffv	$⊢ \underline{Ⅎ} x F (n)$
45	44	nfdm	$⊢ \underline{Ⅎ} x dom F (n)$
46	42 45	nfiin	$⊢ \underline{Ⅎ} x ⋂_{n \in Z} dom F (n)$
47	46	ssrab2f	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ\} \subseteq ⋂_{n \in Z} dom F (n)$
48	7 47	eqsstri	$⊢ D \subseteq ⋂_{n \in Z} dom F (n)$
49		id	$⊢ x \in D \to x \in D$
50	48 49	sseldi	$⊢ x \in D \to x \in ⋂_{n \in Z} dom F (n)$
51	50 23	sylan	$⊢ (x \in D \land n \in Z) \to x \in dom F (n)$
52	51	adantll	$⊢ ((φ \land x \in D) \land n \in Z) \to x \in dom F (n)$
53	41 52	ffvelrnd	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) (x) \in ℝ$
54	49 7	eleqtrdi	$⊢ x \in D \to x \in \{x \in ⋂_{n \in Z} dom F (n) \| sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ\}$
55		rabidim2	$⊢ x \in \{x \in ⋂_{n \in Z} dom F (n) \| sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{} <) \in ℝ\} \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{} <) \in ℝ$
56	54 55	syl	$⊢ x \in D \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ$
57	56	adantl	$⊢ (φ \land x \in D) \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ$
58	50	adantl	$⊢ (φ \land x \in D) \to x \in ⋂_{n \in Z} dom F (n)$
59	58 26	syldan	$⊢ (φ \land x \in D) \to (sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) \in ℝ \leftrightarrow \exists y \in ℝ \forall n \in Z F (n) (x) \leq y)$
60	57 59	mpbid	$⊢ (φ \land x \in D) \to \exists y \in ℝ \forall n \in Z F (n) (x) \leq y$
61	39 40 53 60	supxrrernmpt	$⊢ (φ \land x \in D) \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <) = sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
62	28 61	mpteq12dva	$⊢ φ \to (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ^{*} <)) = (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
63	9 62	eqtrd	$⊢ φ \to G = (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
64		eqid	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
65		eqid	$⊢ (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)) = (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
66	1 2 3 4 5 6 64 65	smfsup	$⊢ φ \to (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)) \in SMblFn (S)$
67	63 66	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfsupxr

Proof