smfpimltmpt

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

	Ref	Expression
Hypotheses	smfpimltmpt.x	$⊢ Ⅎ x φ$
	smfpimltmpt.s	$⊢ φ \to S \in SAlg$
	smfpimltmpt.b	$⊢ (φ \land x \in A) \to B \in V$
	smfpimltmpt.f	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
	smfpimltmpt.r	$⊢ φ \to R \in ℝ$
Assertion	smfpimltmpt	$⊢ φ \to \{x \in A \| B < R\} \in (S ↾_{𝑡} A)$

Proof

Step	Hyp	Ref	Expression
1		smfpimltmpt.x	$⊢ Ⅎ x φ$
2		smfpimltmpt.s	$⊢ φ \to S \in SAlg$
3		smfpimltmpt.b	$⊢ (φ \land x \in A) \to B \in V$
4		smfpimltmpt.f	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
5		smfpimltmpt.r	$⊢ φ \to R \in ℝ$
6		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
7		eqid	$⊢ dom (x \in A ⟼ B) = dom (x \in A ⟼ B)$
8	6 2 4 7 5	smfpreimaltf	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} \in (S ↾_{𝑡} dom (x \in A ⟼ B))$
9		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
10	1 9 3	dmmptdf	$⊢ φ \to dom (x \in A ⟼ B) = A$
11	6	nfdm	$⊢ \underline{Ⅎ} x dom (x \in A ⟼ B)$
12		nfcv	$⊢ \underline{Ⅎ} x A$
13	11 12	rabeqf	$⊢ dom (x \in A ⟼ B) = A \to \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} = \{x \in A \| (x \in A ⟼ B) (x) < R\}$
14	10 13	syl	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} = \{x \in A \| (x \in A ⟼ B) (x) < R\}$
15	9	a1i	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
16	15 3	fvmpt2d	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
17	16	breq1d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ B) (x) < R \leftrightarrow B < R)$
18	1 17	rabbida	$⊢ φ \to \{x \in A \| (x \in A ⟼ B) (x) < R\} = \{x \in A \| B < R\}$
19		eqidd	$⊢ φ \to \{x \in A \| B < R\} = \{x \in A \| B < R\}$
20	14 18 19	3eqtrrd	$⊢ φ \to \{x \in A \| B < R\} = \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\}$
21	10	eqcomd	$⊢ φ \to A = dom (x \in A ⟼ B)$
22	21	oveq2d	$⊢ φ \to S ↾_{𝑡} A = S ↾_{𝑡} dom (x \in A ⟼ B)$
23	20 22	eleq12d	$⊢ φ \to (\{x \in A \| B < R\} \in (S ↾_{𝑡} A) \leftrightarrow \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} \in (S ↾_{𝑡} dom (x \in A ⟼ B)))$
24	8 23	mpbird	$⊢ φ \to \{x \in A \| B < R\} \in (S ↾_{𝑡} A)$

Metamath Proof Explorer

Theorem smfpimltmpt

Proof