smfsuplem2

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

Proof

Step	Hyp	Ref	Expression
1		smfsuplem2.m	$⊢ φ \to M \in ℤ$
2		smfsuplem2.z	$⊢ Z = ℤ_{\geq M}$
3		smfsuplem2.s	$⊢ φ \to S \in SAlg$
4		smfsuplem2.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smfsuplem2.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
6		smfsuplem2.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
7		smfsuplem2.8	$⊢ φ \to A \in ℝ$
8		nfcv	$⊢ \underline{Ⅎ} n F$
9		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
10		eqid	$⊢ SalGen (topGen (ran (.))) = SalGen (topGen (ran (.)))$
11		mnfxr	$⊢ −∞ \in ℝ^{*}$
12	11	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
13	12 7 9 10	iocborel	$⊢ φ \to (−∞, A] \in SalGen (topGen (ran (.)))$
14	8 2 3 4 9 10 13	smfpimcc	$⊢ φ \to \exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))$
15	1	adantr	$⊢ (φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \to M \in ℤ$
16	3	adantr	$⊢ (φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \to S \in SAlg$
17	4	adantr	$⊢ (φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \to F : Z ⟶ SMblFn (S)$
18		fveq2	$⊢ n = m \to F (n) = F (m)$
19	18	dmeqd	$⊢ n = m \to dom F (n) = dom F (m)$
20	19	cbviinv	$⊢ ⋂_{n \in Z} dom F (n) = ⋂_{m \in Z} dom F (m)$
21	20	a1i	$⊢ x = w \to ⋂_{n \in Z} dom F (n) = ⋂_{m \in Z} dom F (m)$
22		fveq2	$⊢ x = w \to F (n) (x) = F (n) (w)$
23	22	breq1d	$⊢ x = w \to (F (n) (x) \leq y \leftrightarrow F (n) (w) \leq y)$
24	23	ralbidv	$⊢ x = w \to (\forall n \in Z F (n) (x) \leq y \leftrightarrow \forall n \in Z F (n) (w) \leq y)$
25	18	fveq1d	$⊢ n = m \to F (n) (w) = F (m) (w)$
26	25	breq1d	$⊢ n = m \to (F (n) (w) \leq y \leftrightarrow F (m) (w) \leq y)$
27	26	cbvralvw	$⊢ \forall n \in Z F (n) (w) \leq y \leftrightarrow \forall m \in Z F (m) (w) \leq y$
28	27	a1i	$⊢ x = w \to (\forall n \in Z F (n) (w) \leq y \leftrightarrow \forall m \in Z F (m) (w) \leq y)$
29	24 28	bitrd	$⊢ x = w \to (\forall n \in Z F (n) (x) \leq y \leftrightarrow \forall m \in Z F (m) (w) \leq y)$
30	29	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)$
31	21 30	cbvrabv2w	$⊢ \{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 y \in ℝ \forall m \in Z F (m) (w) \leq y\}$
32	5 31	eqtri	$⊢ D = \{w \in ⋂_{m \in Z} dom F (m) \| \exists y \in ℝ \forall m \in Z F (m) (w) \leq y\}$
33	22	mpteq2dv	$⊢ x = w \to (n \in Z ⟼ F (n) (x)) = (n \in Z ⟼ F (n) (w))$
34	25	cbvmptv	$⊢ (n \in Z ⟼ F (n) (w)) = (m \in Z ⟼ F (m) (w))$
35	34	a1i	$⊢ x = w \to (n \in Z ⟼ F (n) (w)) = (m \in Z ⟼ F (m) (w))$
36	33 35	eqtrd	$⊢ x = w \to (n \in Z ⟼ F (n) (x)) = (m \in Z ⟼ F (m) (w))$
37	36	rneqd	$⊢ x = w \to ran (n \in Z ⟼ F (n) (x)) = ran (m \in Z ⟼ F (m) (w))$
38	37	supeq1d	$⊢ x = w \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ <) = sup (ran (m \in Z ⟼ F (m) (w)) ℝ <)$
39	38	cbvmptv	$⊢ (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)) = (w \in D ⟼ sup (ran (m \in Z ⟼ F (m) (w)) ℝ <))$
40	6 39	eqtri	$⊢ G = (w \in D ⟼ sup (ran (m \in Z ⟼ F (m) (w)) ℝ <))$
41	7	adantr	$⊢ (φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \to A \in ℝ$
42		simprl	$⊢ (φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \to h : Z ⟶ S$
43		simplrr	$⊢ ((φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \land m \in Z) \to \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n)$
44	18	cnveqd	$⊢ n = m \to {F (n)}^{-1} = {F (m)}^{-1}$
45	44	imaeq1d	$⊢ n = m \to {F (n)}^{-1} [(−∞, A]] = {F (m)}^{-1} [(−∞, A]]$
46		fveq2	$⊢ n = m \to h (n) = h (m)$
47	46 19	ineq12d	$⊢ n = m \to h (n) \cap dom F (n) = h (m) \cap dom F (m)$
48	45 47	eqeq12d	$⊢ n = m \to ({F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n) \leftrightarrow {F (m)}^{-1} [(−∞, A]] = h (m) \cap dom F (m))$
49	48	rspccva	$⊢ (\forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n) \land m \in Z) \to {F (m)}^{-1} [(−∞, A]] = h (m) \cap dom F (m)$
50	43 49	sylancom	$⊢ ((φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \land m \in Z) \to {F (m)}^{-1} [(−∞, A]] = h (m) \cap dom F (m)$
51	15 2 16 17 32 40 41 42 50	smfsuplem1	$⊢ (φ \land (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n))) \to G^{-1} [(−∞, A]] \in (S ↾_{𝑡} D)$
52	51	ex	$⊢ φ \to ((h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n)) \to G^{-1} [(−∞, A]] \in (S ↾_{𝑡} D))$
53	52	exlimdv	$⊢ φ \to (\exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [(−∞, A]] = h (n) \cap dom F (n)) \to G^{-1} [(−∞, A]] \in (S ↾_{𝑡} D))$
54	14 53	mpd	$⊢ φ \to G^{-1} [(−∞, A]] \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfsuplem2

Proof