smfinfdmmbllem

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

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

Proof

Step	Hyp	Ref	Expression
1		smfinfdmmbllem.1	$⊢ Ⅎ n φ$
2		smfinfdmmbllem.2	$⊢ Ⅎ x φ$
3		smfinfdmmbllem.3	$⊢ Ⅎ m φ$
4		smfinfdmmbllem.4	$⊢ \underline{Ⅎ} x F$
5		smfinfdmmbllem.5	$⊢ φ \to M \in ℤ$
6		smfinfdmmbllem.6	$⊢ Z = ℤ_{\geq M}$
7		smfinfdmmbllem.7	$⊢ φ \to S \in SAlg$
8		smfinfdmmbllem.8	$⊢ φ \to F : Z ⟶ SMblFn (S)$
9		smfinfdmmbllem.9	$⊢ (φ \land n \in Z) \to dom F (n) \in S$
10		smfinfdmmbllem.10	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
11		smfinfdmmbllem.11	$⊢ G = (x \in D ⟼ inf (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
12		smfinfdmmbllem.12	$⊢ H = (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| - m < 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 11 12	finfdm2	$⊢ φ \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		nnre	$⊢ m \in ℕ \to m \in ℝ$
41	40	renegcld	$⊢ m \in ℕ \to - m \in ℝ$
42	41	rexrd	$⊢ m \in ℕ \to - m \in ℝ^{*}$
43	42	ad2antlr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to - m \in ℝ^{*}$
44	38 32 39 15 43	smfpimgtxr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to \{x \in dom F (n) \| - m < F (n) (x)\} \in (S ↾_{𝑡} dom F (n))$
45	44	an32s	$⊢ ((φ \land n \in Z) \land m \in ℕ) \to \{x \in dom F (n) \| - m < F (n) (x)\} \in (S ↾_{𝑡} dom F (n))$
46	36 45	fmptd2f	$⊢ (φ \land n \in Z) \to (m \in ℕ ⟼ \{x \in dom F (n) \| - m < F (n) (x)\}) : ℕ ⟶ S ↾_{𝑡} dom F (n)$
47		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
48		nnex	$⊢ ℕ \in V$
49	48	mptex	$⊢ (m \in ℕ ⟼ \{x \in dom F (n) \| - m < F (n) (x)\}) \in V$
50	12	fvmpt2	$⊢ (n \in Z \land (m \in ℕ ⟼ \{x \in dom F (n) \| - m < F (n) (x)\}) \in V) \to H (n) = (m \in ℕ ⟼ \{x \in dom F (n) \| - m < F (n) (x)\})$
51	47 49 50	sylancl	$⊢ (φ \land n \in Z) \to H (n) = (m \in ℕ ⟼ \{x \in dom F (n) \| - m < F (n) (x)\})$
52	51	feq1d	$⊢ (φ \land n \in Z) \to (H (n) : ℕ ⟶ S ↾_{𝑡} dom F (n) \leftrightarrow (m \in ℕ ⟼ \{x \in dom F (n) \| - m < F (n) (x)\}) : ℕ ⟶ S ↾_{𝑡} dom F (n))$
53	46 52	mpbird	$⊢ (φ \land n \in Z) \to H (n) : ℕ ⟶ S ↾_{𝑡} dom F (n)$
54	53	adantlr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to H (n) : ℕ ⟶ S ↾_{𝑡} dom F (n)$
55		simplr	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to m \in ℕ$
56	54 55	ffvelcdmd	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to H (n) (m) \in (S ↾_{𝑡} dom F (n))$
57	34 56	sseldd	$⊢ ((φ \land m \in ℕ) \land n \in Z) \to H (n) (m) \in S$
58	24 25 26 27 29 31 57	saliinclf	$⊢ (φ \land m \in ℕ) \to ⋂_{n \in Z} H (n) (m) \in S$
59	3 19 20 7 22 58	saliunclf	$⊢ φ \to ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m) \in S$
60	18 59	eqeltrd	$⊢ φ \to dom G \in S$

Metamath Proof Explorer

Theorem smfinfdmmbllem

Proof