smfpimioompt

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	smfpimioompt.x	$⊢ Ⅎ x φ$
	smfpimioompt.s	$⊢ φ \to S \in SAlg$
	smfpimioompt.a	$⊢ φ \to A \in V$
	smfpimioompt.b	$⊢ (φ \land x \in A) \to B \in W$
	smfpimioompt.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
	smfpimioompt.l	$⊢ φ \to L \in ℝ^{*}$
	smfpimioompt.r	$⊢ φ \to R \in ℝ^{*}$
Assertion	smfpimioompt	$⊢ φ \to \{x \in A \| B \in (L, R)\} \in (S ↾_{𝑡} A)$

Proof

Step	Hyp	Ref	Expression
1		smfpimioompt.x	$⊢ Ⅎ x φ$
2		smfpimioompt.s	$⊢ φ \to S \in SAlg$
3		smfpimioompt.a	$⊢ φ \to A \in V$
4		smfpimioompt.b	$⊢ (φ \land x \in A) \to B \in W$
5		smfpimioompt.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
6		smfpimioompt.l	$⊢ φ \to L \in ℝ^{*}$
7		smfpimioompt.r	$⊢ φ \to R \in ℝ^{*}$
8		eqid	$⊢ dom (x \in A ⟼ B) = dom (x \in A ⟼ B)$
9	2 5 8	smff	$⊢ φ \to (x \in A ⟼ B) : dom (x \in A ⟼ B) ⟶ ℝ$
10		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
11	1 10 4	dmmptdf	$⊢ φ \to dom (x \in A ⟼ B) = A$
12	11	feq2d	$⊢ φ \to ((x \in A ⟼ B) : dom (x \in A ⟼ B) ⟶ ℝ \leftrightarrow (x \in A ⟼ B) : A ⟶ ℝ)$
13	9 12	mpbid	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℝ$
14	13	fvmptelrn	$⊢ (φ \land x \in A) \to B \in ℝ$
15	14	rexrd	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
16	1 6 7 15	pimiooltgt	$⊢ φ \to \{x \in A \| B \in (L, R)\} = \{x \in A \| B < R\} \cap \{x \in A \| L < B\}$
17		eqid	$⊢ S ↾_{𝑡} A = S ↾_{𝑡} A$
18	2 3 17	subsalsal	$⊢ φ \to S ↾_{𝑡} A \in SAlg$
19	1 2 4 5 7	smfpimltxrmpt	$⊢ φ \to \{x \in A \| B < R\} \in (S ↾_{𝑡} A)$
20	1 2 4 5 6	smfpimgtxrmpt	$⊢ φ \to \{x \in A \| L < B\} \in (S ↾_{𝑡} A)$
21	18 19 20	salincld	$⊢ φ \to \{x \in A \| B < R\} \cap \{x \in A \| L < B\} \in (S ↾_{𝑡} A)$
22	16 21	eqeltrd	$⊢ φ \to \{x \in A \| B \in (L, R)\} \in (S ↾_{𝑡} A)$

Metamath Proof Explorer

Theorem smfpimioompt

Proof