sssmf

Description: The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	sssmf.s	$⊢ φ \to S \in SAlg$
	sssmf.f	$⊢ φ \to F \in SMblFn (S)$
Assertion	sssmf	$⊢ φ \to {F ↾}_{B} \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		sssmf.s	$⊢ φ \to S \in SAlg$
2		sssmf.f	$⊢ φ \to F \in SMblFn (S)$
3		nfv	$⊢ Ⅎ a φ$
4		inss2	$⊢ B \cap dom F \subseteq dom F$
5		eqid	$⊢ dom F = dom F$
6	1 2 5	smfdmss	$⊢ φ \to dom F \subseteq ⋃ S$
7	4 6	sstrid	$⊢ φ \to B \cap dom F \subseteq ⋃ S$
8		resindm	$⊢ {F ↾}_{(B \cap dom F)} = {F ↾}_{B}$
9	8	a1i	$⊢ φ \to {F ↾}_{(B \cap dom F)} = {F ↾}_{B}$
10	1 2 5	smff	$⊢ φ \to F : dom F ⟶ ℝ$
11	4	a1i	$⊢ φ \to B \cap dom F \subseteq dom F$
12	10 11	fssresd	$⊢ φ \to ({F ↾}_{(B \cap dom F)}) : B \cap dom F ⟶ ℝ$
13	9 12	feq1dd	$⊢ φ \to ({F ↾}_{B}) : B \cap dom F ⟶ ℝ$
14	1	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
15	2	adantr	$⊢ (φ \land a \in ℝ) \to F \in SMblFn (S)$
16		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
17	14 15 5 16	smfpreimalt	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) < a\} \in (S ↾_{𝑡} dom F)$
18	2	dmexd	$⊢ φ \to dom F \in V$
19		elrest	$⊢ (S \in SAlg \land dom F \in V) \to (\{x \in dom F \| F (x) < a\} \in (S ↾_{𝑡} dom F) \leftrightarrow \exists w \in S \{x \in dom F \| F (x) < a\} = w \cap dom F)$
20	1 18 19	syl2anc	$⊢ φ \to (\{x \in dom F \| F (x) < a\} \in (S ↾_{𝑡} dom F) \leftrightarrow \exists w \in S \{x \in dom F \| F (x) < a\} = w \cap dom F)$
21	20	adantr	$⊢ (φ \land a \in ℝ) \to (\{x \in dom F \| F (x) < a\} \in (S ↾_{𝑡} dom F) \leftrightarrow \exists w \in S \{x \in dom F \| F (x) < a\} = w \cap dom F)$
22	17 21	mpbid	$⊢ (φ \land a \in ℝ) \to \exists w \in S \{x \in dom F \| F (x) < a\} = w \cap dom F$
23		elinel1	$⊢ x \in (B \cap dom F) \to x \in B$
24	23	fvresd	$⊢ x \in (B \cap dom F) \to ({F ↾}_{B}) (x) = F (x)$
25	24	breq1d	$⊢ x \in (B \cap dom F) \to (({F ↾}_{B}) (x) < a \leftrightarrow F (x) < a)$
26	25	rabbiia	$⊢ \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} = \{x \in (B \cap dom F) \| F (x) < a\}$
27		rabss2	$⊢ B \cap dom F \subseteq dom F \to \{x \in (B \cap dom F) \| F (x) < a\} \subseteq \{x \in dom F \| F (x) < a\}$
28	4 27	ax-mp	$⊢ \{x \in (B \cap dom F) \| F (x) < a\} \subseteq \{x \in dom F \| F (x) < a\}$
29		id	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in dom F \| F (x) < a\} = w \cap dom F$
30		inss1	$⊢ w \cap dom F \subseteq w$
31	29 30	eqsstrdi	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in dom F \| F (x) < a\} \subseteq w$
32	28 31	sstrid	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| F (x) < a\} \subseteq w$
33		ssrab2	$⊢ \{x \in (B \cap dom F) \| F (x) < a\} \subseteq B \cap dom F$
34	33	a1i	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| F (x) < a\} \subseteq B \cap dom F$
35	32 34	ssind	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| F (x) < a\} \subseteq w \cap (B \cap dom F)$
36		nfrab1	$⊢ \underline{Ⅎ} x \{x \in dom F \| F (x) < a\}$
37	36	nfeq1	$⊢ Ⅎ x \{x \in dom F \| F (x) < a\} = w \cap dom F$
38		nfcv	$⊢ \underline{Ⅎ} x (w \cap (B \cap dom F))$
39		nfrab1	$⊢ \underline{Ⅎ} x \{x \in (B \cap dom F) \| F (x) < a\}$
40		elinel2	$⊢ x \in (w \cap (B \cap dom F)) \to x \in (B \cap dom F)$
41	40	adantl	$⊢ (\{x \in dom F \| F (x) < a\} = w \cap dom F \land x \in (w \cap (B \cap dom F))) \to x \in (B \cap dom F)$
42		elinel1	$⊢ x \in (w \cap (B \cap dom F)) \to x \in w$
43	40	elin2d	$⊢ x \in (w \cap (B \cap dom F)) \to x \in dom F$
44	42 43	elind	$⊢ x \in (w \cap (B \cap dom F)) \to x \in (w \cap dom F)$
45	44	adantl	$⊢ (\{x \in dom F \| F (x) < a\} = w \cap dom F \land x \in (w \cap (B \cap dom F))) \to x \in (w \cap dom F)$
46	29	eqcomd	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to w \cap dom F = \{x \in dom F \| F (x) < a\}$
47	46	adantr	$⊢ (\{x \in dom F \| F (x) < a\} = w \cap dom F \land x \in (w \cap (B \cap dom F))) \to w \cap dom F = \{x \in dom F \| F (x) < a\}$
48	45 47	eleqtrd	$⊢ (\{x \in dom F \| F (x) < a\} = w \cap dom F \land x \in (w \cap (B \cap dom F))) \to x \in \{x \in dom F \| F (x) < a\}$
49		rabidim2	$⊢ x \in \{x \in dom F \| F (x) < a\} \to F (x) < a$
50	48 49	syl	$⊢ (\{x \in dom F \| F (x) < a\} = w \cap dom F \land x \in (w \cap (B \cap dom F))) \to F (x) < a$
51	41 50	rabidd	$⊢ (\{x \in dom F \| F (x) < a\} = w \cap dom F \land x \in (w \cap (B \cap dom F))) \to x \in \{x \in (B \cap dom F) \| F (x) < a\}$
52	37 38 39 51	ssdf2	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to w \cap (B \cap dom F) \subseteq \{x \in (B \cap dom F) \| F (x) < a\}$
53	35 52	eqssd	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| F (x) < a\} = w \cap (B \cap dom F)$
54	26 53	eqtrid	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} = w \cap (B \cap dom F)$
55	54	3ad2ant3	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} = w \cap (B \cap dom F)$
56	14	3ad2ant1	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to S \in SAlg$
57		simp1l	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to φ$
58	18 11	ssexd	$⊢ φ \to B \cap dom F \in V$
59	57 58	syl	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to B \cap dom F \in V$
60		simp2	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to w \in S$
61		eqid	$⊢ w \cap (B \cap dom F) = w \cap (B \cap dom F)$
62	56 59 60 61	elrestd	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to w \cap (B \cap dom F) \in (S ↾_{𝑡} (B \cap dom F))$
63	55 62	eqeltrd	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} \in (S ↾_{𝑡} (B \cap dom F))$
64	63	rexlimdv3a	$⊢ (φ \land a \in ℝ) \to (\exists w \in S \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} \in (S ↾_{𝑡} (B \cap dom F)))$
65	22 64	mpd	$⊢ (φ \land a \in ℝ) \to \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} \in (S ↾_{𝑡} (B \cap dom F))$
66	3 1 7 13 65	issmfd	$⊢ φ \to {F ↾}_{B} \in SMblFn (S)$

Metamath Proof Explorer

Theorem sssmf

Proof