smfsupdmmbllem

Description: If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	smfsupdmmbllem.1	$⊢ Ⅎ n φ$
	smfsupdmmbllem.2	$⊢ Ⅎ x φ$
	smfsupdmmbllem.3	$⊢ Ⅎ m φ$
	smfsupdmmbllem.4	$⊢ \underline{Ⅎ} x F$
	smfsupdmmbllem.5	$⊢ φ \to M \in ℤ$
	smfsupdmmbllem.6	$⊢ Z = ℤ_{\geq M}$
	smfsupdmmbllem.7	$⊢ φ \to S \in SAlg$
	smfsupdmmbllem.8	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smfsupdmmbllem.9	$⊢ (φ \land n \in Z) \to dom F (n) \in S$
	smfsupdmmbllem.10	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
	smfsupdmmbllem.11	$⊢ H = (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}))$
	smfsupdmmbllem.12	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
Assertion	smfsupdmmbllem	$⊢ φ \to dom G \in S$

Proof

Step	Hyp	Ref	Expression
1		smfsupdmmbllem.1	$⊢ Ⅎ n φ$
2		smfsupdmmbllem.2	$⊢ Ⅎ x φ$
3		smfsupdmmbllem.3	$⊢ Ⅎ m φ$
4		smfsupdmmbllem.4	$⊢ \underline{Ⅎ} x F$
5		smfsupdmmbllem.5	$⊢ φ \to M \in ℤ$
6		smfsupdmmbllem.6	$⊢ Z = ℤ_{\geq M}$
7		smfsupdmmbllem.7	$⊢ φ \to S \in SAlg$
8		smfsupdmmbllem.8	$⊢ φ \to F : Z ⟶ SMblFn (S)$
9		smfsupdmmbllem.9	$⊢ (φ \land n \in Z) \to dom F (n) \in S$
10		smfsupdmmbllem.10	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
11		smfsupdmmbllem.11	$⊢ H = (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}))$
12		smfsupdmmbllem.12	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
13	7	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
14	8	ffvelcdmda	$⊢ (φ \land n \in Z) \to F (n) \in SMblFn (S)$
15		eqid	$⊢ dom F (n) = dom F (n)$
16	13 14 15	smff	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
17	16	frexr	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ^{*}$
18	1 2 3 4 17 10 12 11	fsupdm2	$⊢ φ \to dom G = ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m)$
19		nfcv	$⊢ \underline{Ⅎ} m S$
20		nfcv	$⊢ \underline{Ⅎ} m ℕ$
21		nnct	$⊢ ℕ ≼ ω$
22	21	a1i	$⊢ φ \to ℕ ≼ ω$
23		nfv	$⊢ Ⅎ n m \in ℕ$
24	1 23	nfan	$⊢ Ⅎ n (φ \land m \in ℕ)$
25		nfcv	$⊢ \underline{Ⅎ} n S$
26		nfcv	$⊢ \underline{Ⅎ} n Z$
27	7	adantr	$⊢ (φ \land m \in ℕ) \to S \in SAlg$
28	6	uzct	$⊢ Z ≼ ω$
29	28	a1i	$⊢ (φ \land m \in ℕ) \to Z ≼ ω$
30	5 6	uzn0d	$⊢ φ \to Z \neq \emptyset$
31	30	adantr	$⊢ (φ \land m \in ℕ) \to Z \neq \emptyset$
32	27	adantr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to S \in SAlg$
33	9	adantlr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to dom F (n) \in S$
34	32 33	salrestss	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to S ↾_{𝑡} dom F (n) \subseteq S$
35		nfv	$⊢ Ⅎ m n \in Z$
36	3 35	nfan	$⊢ Ⅎ m (φ \land n \in Z)$
37		nfcv	$⊢ \underline{Ⅎ} x n$
38	4 37	nffv	$⊢ \underline{Ⅎ} x F (n)$
39	14	adantlr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to F (n) \in SMblFn (S)$
40		nnxr	$⊢ m \in ℕ \to m \in ℝ^{*}$
41	40	ad2antlr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to m \in ℝ^{*}$
42	38 32 39 15 41	smfpimltxr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to \{x \in dom F (n) \| F (n) (x) < m\} \in (S ↾_{𝑡} dom F (n))$
43	42	an32s	$⊢ ((φ \land n \in Z) \land m \in ℕ) \to \{x \in dom F (n) \| F (n) (x) < m\} \in (S ↾_{𝑡} dom F (n))$
44	36 43	fmptd2f	$⊢ (φ \land n \in Z) \to (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}) : ℕ ⟶ S ↾_{𝑡} dom F (n)$
45		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
46		nnex	$⊢ ℕ \in V$
47	46	mptex	$⊢ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}) \in V$
48	11	fvmpt2	$⊢ (n \in Z \land (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}) \in V) \to H (n) = (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\})$
49	45 47 48	sylancl	$⊢ (φ \land n \in Z) \to H (n) = (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\})$
50	49	feq1d	$⊢ (φ \land n \in Z) \to (H (n) : ℕ ⟶ S ↾_{𝑡} dom F (n) \leftrightarrow (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}) : ℕ ⟶ S ↾_{𝑡} dom F (n))$
51	44 50	mpbird	$⊢ (φ \land n \in Z) \to H (n) : ℕ ⟶ S ↾_{𝑡} dom F (n)$
52	51	adantlr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to H (n) : ℕ ⟶ S ↾_{𝑡} dom F (n)$
53		simplr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to m \in ℕ$
54	52 53	ffvelcdmd	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to H (n) (m) \in (S ↾_{𝑡} dom F (n))$
55	34 54	sseldd	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to H (n) (m) \in S$
56	24 25 26 27 29 31 55	saliinclf	$⊢ (φ \land m \in ℕ) \to ⋂_{n \in Z} H (n) (m) \in S$
57	3 19 20 7 22 56	saliunclf	$⊢ φ \to ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m) \in S$
58	18 57	eqeltrd	$⊢ φ \to dom G \in S$

Metamath Proof Explorer

Theorem smfsupdmmbllem

Proof