smfpimgtxr

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) (Revised by Glauco Siliprandi, 15-Dec-2024)

	Ref	Expression
Hypotheses	smfpimgtxr.x	$⊢ \underline{Ⅎ} x F$
	smfpimgtxr.s	$⊢ φ \to S \in SAlg$
	smfpimgtxr.f	$⊢ φ \to F \in SMblFn (S)$
	smfpimgtxr.d	$⊢ D = dom F$
	smfpimgtxr.a	$⊢ φ \to A \in ℝ^{*}$
Assertion	smfpimgtxr	$⊢ φ \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smfpimgtxr.x	$⊢ \underline{Ⅎ} x F$
2		smfpimgtxr.s	$⊢ φ \to S \in SAlg$
3		smfpimgtxr.f	$⊢ φ \to F \in SMblFn (S)$
4		smfpimgtxr.d	$⊢ D = dom F$
5		smfpimgtxr.a	$⊢ φ \to A \in ℝ^{*}$
6		breq1	$⊢ A = −∞ \to (A < F (x) \leftrightarrow −∞ < F (x))$
7	6	rabbidv	$⊢ A = −∞ \to \{x \in D \| A < F (x)\} = \{x \in D \| −∞ < F (x)\}$
8	1	nfdm	$⊢ \underline{Ⅎ} x dom F$
9	4 8	nfcxfr	$⊢ \underline{Ⅎ} x D$
10		nfcv	$⊢ \underline{Ⅎ} y D$
11		nfv	$⊢ Ⅎ y −∞ < F (x)$
12		nfcv	$⊢ \underline{Ⅎ} x −∞$
13		nfcv	$⊢ \underline{Ⅎ} x <$
14		nfcv	$⊢ \underline{Ⅎ} x y$
15	1 14	nffv	$⊢ \underline{Ⅎ} x F (y)$
16	12 13 15	nfbr	$⊢ Ⅎ x −∞ < F (y)$
17		fveq2	$⊢ x = y \to F (x) = F (y)$
18	17	breq2d	$⊢ x = y \to (−∞ < F (x) \leftrightarrow −∞ < F (y))$
19	9 10 11 16 18	cbvrabw	$⊢ \{x \in D \| −∞ < F (x)\} = \{y \in D \| −∞ < F (y)\}$
20		nfv	$⊢ Ⅎ y φ$
21	2 3 4	smff	$⊢ φ \to F : D ⟶ ℝ$
22	21	ffvelcdmda	$⊢ (φ \land y \in D) \to F (y) \in ℝ$
23	20 22	pimgtmnf	$⊢ φ \to \{y \in D \| −∞ < F (y)\} = D$
24	19 23	eqtrid	$⊢ φ \to \{x \in D \| −∞ < F (x)\} = D$
25	7 24	sylan9eqr	$⊢ (φ \land A = −∞) \to \{x \in D \| A < F (x)\} = D$
26	2 3 4	smfdmss	$⊢ φ \to D \subseteq ⋃ S$
27	2 26	subsaluni	$⊢ φ \to D \in (S ↾_{𝑡} D)$
28	27	adantr	$⊢ (φ \land A = −∞) \to D \in (S ↾_{𝑡} D)$
29	25 28	eqeltrd	$⊢ (φ \land A = −∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
30		breq1	$⊢ A = +∞ \to (A < F (x) \leftrightarrow +∞ < F (x))$
31	30	rabbidv	$⊢ A = +∞ \to \{x \in D \| A < F (x)\} = \{x \in D \| +∞ < F (x)\}$
32	1 9 21	pimgtpnf2f	$⊢ φ \to \{x \in D \| +∞ < F (x)\} = \emptyset$
33	31 32	sylan9eqr	$⊢ (φ \land A = +∞) \to \{x \in D \| A < F (x)\} = \emptyset$
34	3	dmexd	$⊢ φ \to dom F \in V$
35	4 34	eqeltrid	$⊢ φ \to D \in V$
36		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
37	2 35 36	subsalsal	$⊢ φ \to S ↾_{𝑡} D \in SAlg$
38	37	0sald	$⊢ φ \to \emptyset \in (S ↾_{𝑡} D)$
39	38	adantr	$⊢ (φ \land A = +∞) \to \emptyset \in (S ↾_{𝑡} D)$
40	33 39	eqeltrd	$⊢ (φ \land A = +∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
41	40	adantlr	$⊢ ((φ \land A \neq −∞) \land A = +∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
42		simpll	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to φ$
43	42 5	syl	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \in ℝ^{*}$
44		simplr	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \neq −∞$
45		neqne	$⊢ \neg A = +∞ \to A \neq +∞$
46	45	adantl	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \neq +∞$
47	43 44 46	xrred	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \in ℝ$
48	2	adantr	$⊢ (φ \land A \in ℝ) \to S \in SAlg$
49	3	adantr	$⊢ (φ \land A \in ℝ) \to F \in SMblFn (S)$
50		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
51	1 48 49 4 50	smfpreimagtf	$⊢ (φ \land A \in ℝ) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
52	42 47 51	syl2anc	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
53	41 52	pm2.61dan	$⊢ (φ \land A \neq −∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
54	29 53	pm2.61dane	$⊢ φ \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfpimgtxr

Proof