Theorem 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	⊢ Ⅎ 𝑥 𝜑
	smfconst.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfconst.a	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
	smfconst.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	smfconst.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	smfconst	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfconst.x	⊢ Ⅎ 𝑥 𝜑
2		smfconst.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfconst.a	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
4		smfconst.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		smfconst.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	5 6	nfcxfr	⊢ Ⅎ 𝑥 𝐹
8		nfv	⊢ Ⅎ 𝑎 𝜑
9	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
10	1 9 5	fmptdf	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
11		nfv	⊢ Ⅎ 𝑥 𝑎 ∈ ℝ
12	1 11	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℝ )
13		nfv	⊢ Ⅎ 𝑥 𝐵 < 𝑎
14	12 13	nfan	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 )
15	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → 𝐵 ∈ ℝ )
16		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → 𝐵 < 𝑎 )
17	14 15 5 16	pimconstlt1	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = 𝐴 )
18		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → 𝐴 = 𝐴 )
19		sseqin2	⊢ ( 𝐴 ⊆ ∪ 𝑆 ↔ ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 )
20	3 19	sylib	⊢ ( 𝜑 → ( ∪ 𝑆 ∩ 𝐴 ) = 𝐴 )
21	20	eqcomd	⊢ ( 𝜑 → 𝐴 = ( ∪ 𝑆 ∩ 𝐴 ) )
22	21	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → 𝐴 = ( ∪ 𝑆 ∩ 𝐴 ) )
23	17 18 22	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( ∪ 𝑆 ∩ 𝐴 ) )
24	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → 𝑆 ∈ SAlg )
25	2	uniexd	⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
26	25 3	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
27	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → 𝐴 ∈ V )
28	24	salunid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → ∪ 𝑆 ∈ 𝑆 )
29		eqid	⊢ ( ∪ 𝑆 ∩ 𝐴 ) = ( ∪ 𝑆 ∩ 𝐴 )
30	24 27 28 29	elrestd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → ( ∪ 𝑆 ∩ 𝐴 ) ∈ ( 𝑆 ↾t 𝐴 ) )
31	23 30	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝐵 < 𝑎 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐴 ) )
32		nfv	⊢ Ⅎ 𝑥 ¬ 𝐵 < 𝑎
33	12 32	nfan	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 )
34	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → 𝐵 ∈ ℝ )
35		rexr	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
36	35	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → 𝑎 ∈ ℝ* )
37		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → ¬ 𝐵 < 𝑎 )
38		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → 𝑎 ∈ ℝ )
39	38 34	lenltd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → ( 𝑎 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑎 ) )
40	37 39	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → 𝑎 ≤ 𝐵 )
41	33 34 5 36 40	pimconstlt0	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ∅ )
42		eqid	⊢ ( 𝑆 ↾t 𝐴 ) = ( 𝑆 ↾t 𝐴 )
43	2 26 42	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐴 ) ∈ SAlg )
44	43	0sald	⊢ ( 𝜑 → ∅ ∈ ( 𝑆 ↾t 𝐴 ) )
45	44	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → ∅ ∈ ( 𝑆 ↾t 𝐴 ) )
46	41 45	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝐵 < 𝑎 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐴 ) )
47	31 46	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐴 ) )
48	7 8 2 3 10 47	issmfdf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )