smfpimltxr

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

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

Proof

Step	Hyp	Ref	Expression
1		smfpimltxr.x	$⊢ \underline{Ⅎ} x F$
2		smfpimltxr.s	$⊢ φ \to S \in SAlg$
3		smfpimltxr.f	$⊢ φ \to F \in SMblFn (S)$
4		smfpimltxr.d	$⊢ D = dom F$
5		smfpimltxr.a	$⊢ φ \to A \in ℝ^{*}$
6		breq2	$⊢ A = +∞ \to (F (x) < A \leftrightarrow F (x) < +∞)$
7	6	rabbidv	$⊢ A = +∞ \to \{x \in D \| F (x) < A\} = \{x \in D \| F (x) < +∞\}$
8	1	nfdm	$⊢ \underline{Ⅎ} x dom F$
9	4 8	nfcxfr	$⊢ \underline{Ⅎ} x D$
10	2 3 4	smff	$⊢ φ \to F : D ⟶ ℝ$
11	1 9 10	pimltpnf2f	$⊢ φ \to \{x \in D \| F (x) < +∞\} = D$
12	7 11	sylan9eqr	$⊢ (φ \land A = +∞) \to \{x \in D \| F (x) < A\} = D$
13	2 3 4	smfdmss	$⊢ φ \to D \subseteq ⋃ S$
14	2 13	subsaluni	$⊢ φ \to D \in (S ↾_{𝑡} D)$
15	14	adantr	$⊢ (φ \land A = +∞) \to D \in (S ↾_{𝑡} D)$
16	12 15	eqeltrd	$⊢ (φ \land A = +∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
17		breq2	$⊢ A = −∞ \to (F (x) < A \leftrightarrow F (x) < −∞)$
18	17	rabbidv	$⊢ A = −∞ \to \{x \in D \| F (x) < A\} = \{x \in D \| F (x) < −∞\}$
19	18	adantl	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < A\} = \{x \in D \| F (x) < −∞\}$
20	10	adantr	$⊢ (φ \land A = −∞) \to F : D ⟶ ℝ$
21	1 9 20	pimltmnf2f	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < −∞\} = \emptyset$
22	19 21	eqtrd	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < A\} = \emptyset$
23	3	dmexd	$⊢ φ \to dom F \in V$
24	4 23	eqeltrid	$⊢ φ \to D \in V$
25		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
26	2 24 25	subsalsal	$⊢ φ \to S ↾_{𝑡} D \in SAlg$
27	26	0sald	$⊢ φ \to \emptyset \in (S ↾_{𝑡} D)$
28	27	adantr	$⊢ (φ \land A = −∞) \to \emptyset \in (S ↾_{𝑡} D)$
29	22 28	eqeltrd	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
30	29	adantlr	$⊢ ((φ \land A \neq +∞) \land A = −∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
31		simpll	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to φ$
32	31 5	syl	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \in ℝ^{*}$
33		neqne	$⊢ \neg A = −∞ \to A \neq −∞$
34	33	adantl	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \neq −∞$
35		simplr	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \neq +∞$
36	32 34 35	xrred	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \in ℝ$
37	2	adantr	$⊢ (φ \land A \in ℝ) \to S \in SAlg$
38	3	adantr	$⊢ (φ \land A \in ℝ) \to F \in SMblFn (S)$
39		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
40	1 37 38 4 39	smfpreimaltf	$⊢ (φ \land A \in ℝ) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
41	31 36 40	syl2anc	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
42	30 41	pm2.61dan	$⊢ (φ \land A \neq +∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
43	16 42	pm2.61dane	$⊢ φ \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfpimltxr

Proof