smfpimioo

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimioo.s	$⊢ φ \to S \in SAlg$
	smfpimioo.f	$⊢ φ \to F \in SMblFn (S)$
	smfpimioo.d	$⊢ D = dom F$
	smfpimioo.a	$⊢ φ \to A \in ℝ^{*}$
	smfpimioo.b	$⊢ φ \to B \in ℝ^{*}$
Assertion	smfpimioo	$⊢ φ \to F^{-1} [(A, B)] \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smfpimioo.s	$⊢ φ \to S \in SAlg$
2		smfpimioo.f	$⊢ φ \to F \in SMblFn (S)$
3		smfpimioo.d	$⊢ D = dom F$
4		smfpimioo.a	$⊢ φ \to A \in ℝ^{*}$
5		smfpimioo.b	$⊢ φ \to B \in ℝ^{*}$
6	1 2 3	smff	$⊢ φ \to F : D ⟶ ℝ$
7	6	feqmptd	$⊢ φ \to F = (x \in D ⟼ F (x))$
8	7	cnveqd	$⊢ φ \to F^{-1} = {(x \in D ⟼ F (x))}^{-1}$
9	8	imaeq1d	$⊢ φ \to F^{-1} [(A, B)] = {(x \in D ⟼ F (x))}^{-1} [(A, B)]$
10		eqid	$⊢ (x \in D ⟼ F (x)) = (x \in D ⟼ F (x))$
11	10	mptpreima	$⊢ {(x \in D ⟼ F (x))}^{-1} [(A, B)] = \{x \in D \| F (x) \in (A, B)\}$
12	11	a1i	$⊢ φ \to {(x \in D ⟼ F (x))}^{-1} [(A, B)] = \{x \in D \| F (x) \in (A, B)\}$
13	9 12	eqtrd	$⊢ φ \to F^{-1} [(A, B)] = \{x \in D \| F (x) \in (A, B)\}$
14		nfv	$⊢ Ⅎ x φ$
15	1	uniexd	$⊢ φ \to ⋃ S \in V$
16	1 2 3	smfdmss	$⊢ φ \to D \subseteq ⋃ S$
17	15 16	ssexd	$⊢ φ \to D \in V$
18	6	ffvelrnda	$⊢ (φ \land x \in D) \to F (x) \in ℝ$
19	7 2	eqeltrrd	$⊢ φ \to (x \in D ⟼ F (x)) \in SMblFn (S)$
20	14 1 17 18 19 4 5	smfpimioompt	$⊢ φ \to \{x \in D \| F (x) \in (A, B)\} \in (S ↾_{𝑡} D)$
21	13 20	eqeltrd	$⊢ φ \to F^{-1} [(A, B)] \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfpimioo

Proof