smfsuplem3

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

Proof

Step	Hyp	Ref	Expression
1		smfsuplem3.m	$⊢ φ \to M \in ℤ$
2		smfsuplem3.z	$⊢ Z = ℤ_{\geq M}$
3		smfsuplem3.s	$⊢ φ \to S \in SAlg$
4		smfsuplem3.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smfsuplem3.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
6		smfsuplem3.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
7		nfv	$⊢ Ⅎ a φ$
8		ssrab2	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} \subseteq ⋂_{n \in Z} dom F (n)$
9	5 8	eqsstri	$⊢ D \subseteq ⋂_{n \in Z} dom F (n)$
10	9	a1i	$⊢ φ \to D \subseteq ⋂_{n \in Z} dom F (n)$
11		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
12	1 11	syl	$⊢ φ \to M \in ℤ_{\geq M}$
13	12 2	eleqtrrdi	$⊢ φ \to M \in Z$
14		fveq2	$⊢ n = M \to F (n) = F (M)$
15	14	dmeqd	$⊢ n = M \to dom F (n) = dom F (M)$
16	4 13	ffvelrnd	$⊢ φ \to F (M) \in SMblFn (S)$
17		eqid	$⊢ dom F (M) = dom F (M)$
18	3 16 17	smfdmss	$⊢ φ \to dom F (M) \subseteq ⋃ S$
19	13 15 18	iinssd	$⊢ φ \to ⋂_{n \in Z} dom F (n) \subseteq ⋃ S$
20	10 19	sstrd	$⊢ φ \to D \subseteq ⋃ S$
21		nfv	$⊢ Ⅎ n (φ \land x \in D)$
22	13	ne0d	$⊢ φ \to Z \neq \emptyset$
23	22	adantr	$⊢ (φ \land x \in D) \to Z \neq \emptyset$
24	3	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
25	4	ffvelrnda	$⊢ (φ \land n \in Z) \to F (n) \in SMblFn (S)$
26		eqid	$⊢ dom F (n) = dom F (n)$
27	24 25 26	smff	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
28	27	adantlr	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
29		iinss2	$⊢ n \in Z \to ⋂_{n \in Z} dom F (n) \subseteq dom F (n)$
30	29	adantl	$⊢ (x \in D \land n \in Z) \to ⋂_{n \in Z} dom F (n) \subseteq dom F (n)$
31	9	sseli	$⊢ x \in D \to x \in ⋂_{n \in Z} dom F (n)$
32	31	adantr	$⊢ (x \in D \land n \in Z) \to x \in ⋂_{n \in Z} dom F (n)$
33	30 32	sseldd	$⊢ (x \in D \land n \in Z) \to x \in dom F (n)$
34	33	adantll	$⊢ ((φ \land x \in D) \land n \in Z) \to x \in dom F (n)$
35	28 34	ffvelrnd	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) (x) \in ℝ$
36	5	rabeq2i	$⊢ x \in D \leftrightarrow (x \in ⋂_{n \in Z} dom F (n) \land \exists y \in ℝ \forall n \in Z F (n) (x) \leq y)$
37	36	simprbi	$⊢ x \in D \to \exists y \in ℝ \forall n \in Z F (n) (x) \leq y$
38	37	adantl	$⊢ (φ \land x \in D) \to \exists y \in ℝ \forall n \in Z F (n) (x) \leq y$
39	21 23 35 38	suprclrnmpt	$⊢ (φ \land x \in D) \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ <) \in ℝ$
40	39 6	fmptd	$⊢ φ \to G : D ⟶ ℝ$
41	1	adantr	$⊢ (φ \land a \in ℝ) \to M \in ℤ$
42	3	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
43	4	adantr	$⊢ (φ \land a \in ℝ) \to F : Z ⟶ SMblFn (S)$
44		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
45	41 2 42 43 5 6 44	smfsuplem2	$⊢ (φ \land a \in ℝ) \to G^{-1} [(−∞, a]] \in (S ↾_{𝑡} D)$
46	7 3 20 40 45	issmfle2d	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfsuplem3

Proof