smfpimgtxrmpt

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, 26-Jun-2021)

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

Proof

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

Metamath Proof Explorer

Theorem smfpimgtxrmpt

Proof