smfpimltxrmpt

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

Proof

Step	Hyp	Ref	Expression
1		smfpimltxrmpt.x	$⊢ Ⅎ x φ$
2		smfpimltxrmpt.s	$⊢ φ \to S \in SAlg$
3		smfpimltxrmpt.b	$⊢ (φ \land x \in A) \to B \in V$
4		smfpimltxrmpt.f	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
5		smfpimltxrmpt.r	$⊢ φ \to R \in ℝ^{*}$
6		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
7	6	nfdm	$⊢ \underline{Ⅎ} x dom (x \in A ⟼ B)$
8		nfcv	$⊢ \underline{Ⅎ} y dom (x \in A ⟼ B)$
9		nfv	$⊢ Ⅎ y (x \in A ⟼ B) (x) < R$
10		nfcv	$⊢ \underline{Ⅎ} x y$
11	6 10	nffv	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (y)$
12		nfcv	$⊢ \underline{Ⅎ} x <$
13		nfcv	$⊢ \underline{Ⅎ} x R$
14	11 12 13	nfbr	$⊢ Ⅎ x (x \in A ⟼ B) (y) < R$
15		fveq2	$⊢ x = y \to (x \in A ⟼ B) (x) = (x \in A ⟼ B) (y)$
16	15	breq1d	$⊢ x = y \to ((x \in A ⟼ B) (x) < R \leftrightarrow (x \in A ⟼ B) (y) < R)$
17	7 8 9 14 16	cbvrabw	$⊢ \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} = \{y \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (y) < R\}$
18	17	a1i	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} = \{y \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (y) < R\}$
19		nfcv	$⊢ \underline{Ⅎ} y (x \in A ⟼ B)$
20		eqid	$⊢ dom (x \in A ⟼ B) = dom (x \in A ⟼ B)$
21	19 2 4 20 5	smfpimltxr	$⊢ φ \to \{y \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (y) < R\} \in (S ↾_{𝑡} dom (x \in A ⟼ B))$
22	18 21	eqeltrd	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} \in (S ↾_{𝑡} dom (x \in A ⟼ B))$
23		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
24	1 23 3	dmmptdf	$⊢ φ \to dom (x \in A ⟼ B) = A$
25		nfcv	$⊢ \underline{Ⅎ} x A$
26	7 25	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\}$
27	24 26	syl	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\} = \{x \in A \| (x \in A ⟼ B) (x) < R\}$
28	23	a1i	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
29	28 3	fvmpt2d	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
30	29	breq1d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ B) (x) < R \leftrightarrow B < R)$
31	1 30	rabbida	$⊢ φ \to \{x \in A \| (x \in A ⟼ B) (x) < R\} = \{x \in A \| B < R\}$
32		eqidd	$⊢ φ \to \{x \in A \| B < R\} = \{x \in A \| B < R\}$
33	27 31 32	3eqtrrd	$⊢ φ \to \{x \in A \| B < R\} = \{x \in dom (x \in A ⟼ B) \| (x \in A ⟼ B) (x) < R\}$
34	24	eqcomd	$⊢ φ \to A = dom (x \in A ⟼ B)$
35	34	oveq2d	$⊢ φ \to S ↾_{𝑡} A = S ↾_{𝑡} dom (x \in A ⟼ B)$
36	33 35	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)))$
37	22 36	mpbird	$⊢ φ \to \{x \in A \| B < R\} \in (S ↾_{𝑡} A)$

Metamath Proof Explorer

Theorem smfpimltxrmpt

Proof