smfpimgtxrmptf

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

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

Proof

Step	Hyp	Ref	Expression
1		smfpimgtxrmptf.x	$⊢ Ⅎ x φ$
2		smfpimgtxrmptf.1	$⊢ \underline{Ⅎ} x A$
3		smfpimgtxrmptf.s	$⊢ φ \to S \in SAlg$
4		smfpimgtxrmptf.b	$⊢ (φ \land x \in A) \to B \in V$
5		smfpimgtxrmptf.f	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
6		smfpimgtxrmptf.l	$⊢ φ \to L \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 L < (x \in A ⟼ B) (x)$
11		nfcv	$⊢ \underline{Ⅎ} x L$
12		nfcv	$⊢ \underline{Ⅎ} x <$
13		nfcv	$⊢ \underline{Ⅎ} x y$
14	7 13	nffv	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (y)$
15	11 12 14	nfbr	$⊢ Ⅎ x L < (x \in A ⟼ B) (y)$
16		fveq2	$⊢ x = y \to (x \in A ⟼ B) (x) = (x \in A ⟼ B) (y)$
17	16	breq2d	$⊢ x = y \to (L < (x \in A ⟼ B) (x) \leftrightarrow L < (x \in A ⟼ B) (y))$
18	8 9 10 15 17	cbvrabw	$⊢ \{x \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (x)\} = \{y \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (y)\}$
19	18	a1i	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (x)\} = \{y \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (y)\}$
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	smfpimgtxr	$⊢ φ \to \{y \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (y)\} \in (S ↾_{𝑡} dom (x \in A ⟼ B))$
23	19 22	eqeltrd	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (x)\} \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) \| L < (x \in A ⟼ B) (x)\} = \{x \in A \| L < (x \in A ⟼ B) (x)\}$
27	25 26	syl	$⊢ φ \to \{x \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (x)\} = \{x \in A \| L < (x \in A ⟼ B) (x)\}$
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	breq2d	$⊢ (φ \land x \in A) \to (L < (x \in A ⟼ B) (x) \leftrightarrow L < B)$
32	1 31	rabbida	$⊢ φ \to \{x \in A \| L < (x \in A ⟼ B) (x)\} = \{x \in A \| L < B\}$
33		eqidd	$⊢ φ \to \{x \in A \| L < B\} = \{x \in A \| L < B\}$
34	27 32 33	3eqtrrd	$⊢ φ \to \{x \in A \| L < B\} = \{x \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (x)\}$
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 \| L < B\} \in (S ↾_{𝑡} A) \leftrightarrow \{x \in dom (x \in A ⟼ B) \| L < (x \in A ⟼ B) (x)\} \in (S ↾_{𝑡} dom (x \in A ⟼ B)))$
38	23 37	mpbird	$⊢ φ \to \{x \in A \| L < B\} \in (S ↾_{𝑡} A)$

Metamath Proof Explorer

Theorem smfpimgtxrmptf

Proof