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	1 2 5	smff	$⊢ φ \to F : dom F ⟶ ℝ$
9	4	a1i	$⊢ φ \to B \cap dom F \subseteq dom F$
10		fssres	$⊢ (F : dom F ⟶ ℝ \land B \cap dom F \subseteq dom F) \to ({F ↾}_{(B \cap dom F)}) : B \cap dom F ⟶ ℝ$
11	8 9 10	syl2anc	$⊢ φ \to ({F ↾}_{(B \cap dom F)}) : B \cap dom F ⟶ ℝ$
12	8	freld	$⊢ φ \to Rel F$
13		resindm	$⊢ Rel F \to {F ↾}_{(B \cap dom F)} = {F ↾}_{B}$
14	12 13	syl	$⊢ φ \to {F ↾}_{(B \cap dom F)} = {F ↾}_{B}$
15	14	eqcomd	$⊢ φ \to {F ↾}_{B} = {F ↾}_{(B \cap dom F)}$
16		dmres	$⊢ dom ({F ↾}_{B}) = B \cap dom F$
17	16	a1i	$⊢ φ \to dom ({F ↾}_{B}) = B \cap dom F$
18	15 17	feq12d	$⊢ φ \to (({F ↾}_{B}) : dom ({F ↾}_{B}) ⟶ ℝ \leftrightarrow ({F ↾}_{(B \cap dom F)}) : B \cap dom F ⟶ ℝ)$
19	11 18	mpbird	$⊢ φ \to ({F ↾}_{B}) : dom ({F ↾}_{B}) ⟶ ℝ$
20	17	feq2d	$⊢ φ \to (({F ↾}_{B}) : dom ({F ↾}_{B}) ⟶ ℝ \leftrightarrow ({F ↾}_{B}) : B \cap dom F ⟶ ℝ)$
21	19 20	mpbid	$⊢ φ \to ({F ↾}_{B}) : B \cap dom F ⟶ ℝ$
22	1	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
23	2	adantr	$⊢ (φ \land a \in ℝ) \to F \in SMblFn (S)$
24		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
25	22 23 5 24	smfpreimalt	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) < a\} \in (S ↾_{𝑡} dom F)$
26	2	dmexd	$⊢ φ \to dom F \in V$
27		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)$
28	1 26 27	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)$
29	28	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)$
30	25 29	mpbid	$⊢ (φ \land a \in ℝ) \to \exists w \in S \{x \in dom F \| F (x) < a\} = w \cap dom F$
31		elinel1	$⊢ x \in (B \cap dom F) \to x \in B$
32	31	fvresd	$⊢ x \in (B \cap dom F) \to ({F ↾}_{B}) (x) = F (x)$
33	32	breq1d	$⊢ x \in (B \cap dom F) \to (({F ↾}_{B}) (x) < a \leftrightarrow F (x) < a)$
34	33	rabbiia	$⊢ \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} = \{x \in (B \cap dom F) \| F (x) < a\}$
35	34	a1i	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} = \{x \in (B \cap dom F) \| F (x) < a\}$
36		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\}$
37	4 36	ax-mp	$⊢ \{x \in (B \cap dom F) \| F (x) < a\} \subseteq \{x \in dom F \| F (x) < a\}$
38		id	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in dom F \| F (x) < a\} = w \cap dom F$
39		inss1	$⊢ w \cap dom F \subseteq w$
40	39	a1i	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to w \cap dom F \subseteq w$
41	38 40	eqsstrd	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in dom F \| F (x) < a\} \subseteq w$
42	37 41	sstrid	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \{x \in (B \cap dom F) \| F (x) < a\} \subseteq w$
43		ssrab2	$⊢ \{x \in (B \cap dom F) \| F (x) < a\} \subseteq B \cap dom F$
44	43	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$
45	42 44	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)$
46		nfrab1	$⊢ \underline{Ⅎ} x \{x \in dom F \| F (x) < a\}$
47		nfcv	$⊢ \underline{Ⅎ} x (w \cap dom F)$
48	46 47	nfeq	$⊢ Ⅎ x \{x \in dom F \| F (x) < a\} = w \cap dom F$
49		elinel2	$⊢ x \in (w \cap (B \cap dom F)) \to x \in (B \cap dom F)$
50	49	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)$
51		elinel1	$⊢ x \in (w \cap (B \cap dom F)) \to x \in w$
52	4	sseli	$⊢ x \in (B \cap dom F) \to x \in dom F$
53	49 52	syl	$⊢ x \in (w \cap (B \cap dom F)) \to x \in dom F$
54	51 53	elind	$⊢ x \in (w \cap (B \cap dom F)) \to x \in (w \cap dom F)$
55	54	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)$
56	38	eqcomd	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to w \cap dom F = \{x \in dom F \| F (x) < a\}$
57	56	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\}$
58	55 57	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\}$
59		rabid	$⊢ x \in \{x \in dom F \| F (x) < a\} \leftrightarrow (x \in dom F \land F (x) < a)$
60	59	biimpi	$⊢ x \in \{x \in dom F \| F (x) < a\} \to (x \in dom F \land F (x) < a)$
61	60	simprd	$⊢ x \in \{x \in dom F \| F (x) < a\} \to F (x) < a$
62	58 61	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$
63	50 62	jca	$⊢ (\{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) \land F (x) < a)$
64		rabid	$⊢ x \in \{x \in (B \cap dom F) \| F (x) < a\} \leftrightarrow (x \in (B \cap dom F) \land F (x) < a)$
65	63 64	sylibr	$⊢ (\{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\}$
66	65	ex	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to (x \in (w \cap (B \cap dom F)) \to x \in \{x \in (B \cap dom F) \| F (x) < a\})$
67	48 66	ralrimi	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \forall x \in (w \cap (B \cap dom F)) x \in \{x \in (B \cap dom F) \| F (x) < a\}$
68		nfcv	$⊢ \underline{Ⅎ} x (w \cap (B \cap dom F))$
69		nfrab1	$⊢ \underline{Ⅎ} x \{x \in (B \cap dom F) \| F (x) < a\}$
70	68 69	dfss3f	$⊢ w \cap (B \cap dom F) \subseteq \{x \in (B \cap dom F) \| F (x) < a\} \leftrightarrow \forall x \in (w \cap (B \cap dom F)) x \in \{x \in (B \cap dom F) \| F (x) < a\}$
71	67 70	sylibr	$⊢ \{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\}$
72	71	sseld	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to (x \in (w \cap (B \cap dom F)) \to x \in \{x \in (B \cap dom F) \| F (x) < a\})$
73	48 72	ralrimi	$⊢ \{x \in dom F \| F (x) < a\} = w \cap dom F \to \forall x \in (w \cap (B \cap dom F)) x \in \{x \in (B \cap dom F) \| F (x) < a\}$
74	73 70	sylibr	$⊢ \{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\}$
75	45 74	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)$
76	35 75	eqtrd	$⊢ \{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)$
77	76	adantl	$⊢ ((φ \land a \in ℝ) \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)$
78	77	3adant2	$⊢ ((φ \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)$
79	22	3ad2ant1	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to S \in SAlg$
80		simp1l	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to φ$
81	26 9	ssexd	$⊢ φ \to B \cap dom F \in V$
82	80 81	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$
83		simp2	$⊢ ((φ \land a \in ℝ) \land w \in S \land \{x \in dom F \| F (x) < a\} = w \cap dom F) \to w \in S$
84		eqid	$⊢ w \cap (B \cap dom F) = w \cap (B \cap dom F)$
85	79 82 83 84	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))$
86	78 85	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))$
87	86	3exp	$⊢ (φ \land a \in ℝ) \to (w \in S \to (\{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))))$
88	87	rexlimdv	$⊢ (φ \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)))$
89	30 88	mpd	$⊢ (φ \land a \in ℝ) \to \{x \in (B \cap dom F) \| ({F ↾}_{B}) (x) < a\} \in (S ↾_{𝑡} (B \cap dom F))$
90	3 1 7 21 89	issmfd	$⊢ φ \to {F ↾}_{B} \in SMblFn (S)$

Metamath Proof Explorer

Theorem sssmf

Proof