smfres

Description: The restriction of sigma-measurable function is sigma-measurable. Proposition 121E (h) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfres.s	$⊢ φ \to S \in SAlg$
	smfres.f	$⊢ φ \to F \in SMblFn (S)$
	smfres.a	$⊢ φ \to A \in V$
Assertion	smfres	$⊢ φ \to {F ↾}_{A} \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfres.s	$⊢ φ \to S \in SAlg$
2		smfres.f	$⊢ φ \to F \in SMblFn (S)$
3		smfres.a	$⊢ φ \to A \in V$
4		nfv	$⊢ Ⅎ a φ$
5		inss1	$⊢ dom F \cap A \subseteq dom F$
6	5	a1i	$⊢ φ \to dom F \cap A \subseteq dom F$
7		eqid	$⊢ dom F = dom F$
8	1 2 7	smfdmss	$⊢ φ \to dom F \subseteq ⋃ S$
9	6 8	sstrd	$⊢ φ \to dom F \cap A \subseteq ⋃ S$
10	1 2 7	smff	$⊢ φ \to F : dom F ⟶ ℝ$
11		fresin	$⊢ F : dom F ⟶ ℝ \to ({F ↾}_{A}) : dom F \cap A ⟶ ℝ$
12	10 11	syl	$⊢ φ \to ({F ↾}_{A}) : dom F \cap A ⟶ ℝ$
13		ovexd	$⊢ (φ \land a \in ℝ) \to S ↾_{𝑡} dom F \in V$
14	3	adantr	$⊢ (φ \land a \in ℝ) \to A \in V$
15	1	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
16	2	adantr	$⊢ (φ \land a \in ℝ) \to F \in SMblFn (S)$
17		mnfxr	$⊢ −∞ \in ℝ^{*}$
18	17	a1i	$⊢ (φ \land a \in ℝ) \to −∞ \in ℝ^{*}$
19		rexr	$⊢ a \in ℝ \to a \in ℝ^{*}$
20	19	adantl	$⊢ (φ \land a \in ℝ) \to a \in ℝ^{*}$
21	15 16 7 18 20	smfpimioo	$⊢ (φ \land a \in ℝ) \to F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
22		eqid	$⊢ F^{-1} [(−∞, a)] \cap A = F^{-1} [(−∞, a)] \cap A$
23	13 14 21 22	elrestd	$⊢ (φ \land a \in ℝ) \to F^{-1} [(−∞, a)] \cap A \in ((S ↾_{𝑡} dom F) ↾_{𝑡} A)$
24	10	ffund	$⊢ φ \to Fun F$
25		respreima	$⊢ Fun F \to {({F ↾}_{A})}^{-1} [(−∞, a)] = F^{-1} [(−∞, a)] \cap A$
26	24 25	syl	$⊢ φ \to {({F ↾}_{A})}^{-1} [(−∞, a)] = F^{-1} [(−∞, a)] \cap A$
27	26	eqcomd	$⊢ φ \to F^{-1} [(−∞, a)] \cap A = {({F ↾}_{A})}^{-1} [(−∞, a)]$
28	27	adantr	$⊢ (φ \land a \in ℝ) \to F^{-1} [(−∞, a)] \cap A = {({F ↾}_{A})}^{-1} [(−∞, a)]$
29	12	adantr	$⊢ (φ \land a \in ℝ) \to ({F ↾}_{A}) : dom F \cap A ⟶ ℝ$
30	29 20	preimaioomnf	$⊢ (φ \land a \in ℝ) \to {({F ↾}_{A})}^{-1} [(−∞, a)] = \{x \in (dom F \cap A) \| ({F ↾}_{A}) (x) < a\}$
31	28 30	eqtr2d	$⊢ (φ \land a \in ℝ) \to \{x \in (dom F \cap A) \| ({F ↾}_{A}) (x) < a\} = F^{-1} [(−∞, a)] \cap A$
32	2	dmexd	$⊢ φ \to dom F \in V$
33		restco	$⊢ (S \in SAlg \land dom F \in V \land A \in V) \to (S ↾_{𝑡} dom F) ↾_{𝑡} A = S ↾_{𝑡} (dom F \cap A)$
34	1 32 3 33	syl3anc	$⊢ φ \to (S ↾_{𝑡} dom F) ↾_{𝑡} A = S ↾_{𝑡} (dom F \cap A)$
35	34	adantr	$⊢ (φ \land a \in ℝ) \to (S ↾_{𝑡} dom F) ↾_{𝑡} A = S ↾_{𝑡} (dom F \cap A)$
36	35	eqcomd	$⊢ (φ \land a \in ℝ) \to S ↾_{𝑡} (dom F \cap A) = (S ↾_{𝑡} dom F) ↾_{𝑡} A$
37	31 36	eleq12d	$⊢ (φ \land a \in ℝ) \to (\{x \in (dom F \cap A) \| ({F ↾}_{A}) (x) < a\} \in (S ↾_{𝑡} (dom F \cap A)) \leftrightarrow F^{-1} [(−∞, a)] \cap A \in ((S ↾_{𝑡} dom F) ↾_{𝑡} A))$
38	23 37	mpbird	$⊢ (φ \land a \in ℝ) \to \{x \in (dom F \cap A) \| ({F ↾}_{A}) (x) < a\} \in (S ↾_{𝑡} (dom F \cap A))$
39	4 1 9 12 38	issmfd	$⊢ φ \to {F ↾}_{A} \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfres

Proof