smfconst

Description: Given a sigma-algebra over a base set X, every partial real-valued constant function is measurable. Proposition 121E (a) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfconst.x	$⊢ Ⅎ x φ$
	smfconst.s	$⊢ φ \to S \in SAlg$
	smfconst.a	$⊢ φ \to A \subseteq ⋃ S$
	smfconst.b	$⊢ φ \to B \in ℝ$
	smfconst.f	$⊢ F = (x \in A ⟼ B)$
Assertion	smfconst	$⊢ φ \to F \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfconst.x	$⊢ Ⅎ x φ$
2		smfconst.s	$⊢ φ \to S \in SAlg$
3		smfconst.a	$⊢ φ \to A \subseteq ⋃ S$
4		smfconst.b	$⊢ φ \to B \in ℝ$
5		smfconst.f	$⊢ F = (x \in A ⟼ B)$
6		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
7	5 6	nfcxfr	$⊢ \underline{Ⅎ} x F$
8		nfv	$⊢ Ⅎ a φ$
9	4	adantr	$⊢ (φ \land x \in A) \to B \in ℝ$
10	1 9 5	fmptdf	$⊢ φ \to F : A ⟶ ℝ$
11		nfv	$⊢ Ⅎ x a \in ℝ$
12	1 11	nfan	$⊢ Ⅎ x (φ \land a \in ℝ)$
13		nfv	$⊢ Ⅎ x B < a$
14	12 13	nfan	$⊢ Ⅎ x ((φ \land a \in ℝ) \land B < a)$
15	4	ad2antrr	$⊢ ((φ \land a \in ℝ) \land B < a) \to B \in ℝ$
16		simpr	$⊢ ((φ \land a \in ℝ) \land B < a) \to B < a$
17	14 15 5 16	pimconstlt1	$⊢ ((φ \land a \in ℝ) \land B < a) \to \{x \in A \| F (x) < a\} = A$
18		eqidd	$⊢ ((φ \land a \in ℝ) \land B < a) \to A = A$
19		sseqin2	$⊢ A \subseteq ⋃ S \leftrightarrow ⋃ S \cap A = A$
20	3 19	sylib	$⊢ φ \to ⋃ S \cap A = A$
21	20	eqcomd	$⊢ φ \to A = ⋃ S \cap A$
22	21	ad2antrr	$⊢ ((φ \land a \in ℝ) \land B < a) \to A = ⋃ S \cap A$
23	17 18 22	3eqtrd	$⊢ ((φ \land a \in ℝ) \land B < a) \to \{x \in A \| F (x) < a\} = ⋃ S \cap A$
24	2	ad2antrr	$⊢ ((φ \land a \in ℝ) \land B < a) \to S \in SAlg$
25	2	uniexd	$⊢ φ \to ⋃ S \in V$
26	25 3	ssexd	$⊢ φ \to A \in V$
27	26	ad2antrr	$⊢ ((φ \land a \in ℝ) \land B < a) \to A \in V$
28	24	salunid	$⊢ ((φ \land a \in ℝ) \land B < a) \to ⋃ S \in S$
29		eqid	$⊢ ⋃ S \cap A = ⋃ S \cap A$
30	24 27 28 29	elrestd	$⊢ ((φ \land a \in ℝ) \land B < a) \to ⋃ S \cap A \in (S ↾_{𝑡} A)$
31	23 30	eqeltrd	$⊢ ((φ \land a \in ℝ) \land B < a) \to \{x \in A \| F (x) < a\} \in (S ↾_{𝑡} A)$
32		nfv	$⊢ Ⅎ x \neg B < a$
33	12 32	nfan	$⊢ Ⅎ x ((φ \land a \in ℝ) \land \neg B < a)$
34	4	ad2antrr	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to B \in ℝ$
35		rexr	$⊢ a \in ℝ \to a \in ℝ^{*}$
36	35	ad2antlr	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to a \in ℝ^{*}$
37		simpr	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to \neg B < a$
38		simplr	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to a \in ℝ$
39	38 34	lenltd	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to (a \leq B \leftrightarrow \neg B < a)$
40	37 39	mpbird	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to a \leq B$
41	33 34 5 36 40	pimconstlt0	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to \{x \in A \| F (x) < a\} = \emptyset$
42		eqid	$⊢ S ↾_{𝑡} A = S ↾_{𝑡} A$
43	2 26 42	subsalsal	$⊢ φ \to S ↾_{𝑡} A \in SAlg$
44	43	0sald	$⊢ φ \to \emptyset \in (S ↾_{𝑡} A)$
45	44	ad2antrr	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to \emptyset \in (S ↾_{𝑡} A)$
46	41 45	eqeltrd	$⊢ ((φ \land a \in ℝ) \land \neg B < a) \to \{x \in A \| F (x) < a\} \in (S ↾_{𝑡} A)$
47	31 46	pm2.61dan	$⊢ (φ \land a \in ℝ) \to \{x \in A \| F (x) < a\} \in (S ↾_{𝑡} A)$
48	7 8 2 3 10 47	issmfdf	$⊢ φ \to F \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfconst

Proof