smfpimltxrmptf

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, 20-Dec-2024)

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

Proof

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

Metamath Proof Explorer

Theorem smfpimltxrmptf

Proof