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)

	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	7	adantl	$⊢ (φ \land A = +∞) \to \{x \in D \| F (x) < A\} = \{x \in D \| F (x) < +∞\}$
9	1 2 4	issmff	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)))$
10	3 9	mpbid	$⊢ φ \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))$
11	10	simp2d	$⊢ φ \to F : D ⟶ ℝ$
12	1 11	pimltpnf2	$⊢ φ \to \{x \in D \| F (x) < +∞\} = D$
13	12	adantr	$⊢ (φ \land A = +∞) \to \{x \in D \| F (x) < +∞\} = D$
14		eqidd	$⊢ (φ \land A = +∞) \to D = D$
15	8 13 14	3eqtrd	$⊢ (φ \land A = +∞) \to \{x \in D \| F (x) < A\} = D$
16	10	simp1d	$⊢ φ \to D \subseteq ⋃ S$
17	2 16	restuni4	$⊢ φ \to ⋃ (S ↾_{𝑡} D) = D$
18	17	eqcomd	$⊢ φ \to D = ⋃ (S ↾_{𝑡} D)$
19	3	dmexd	$⊢ φ \to dom F \in V$
20	4 19	eqeltrid	$⊢ φ \to D \in V$
21		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
22	2 20 21	subsalsal	$⊢ φ \to S ↾_{𝑡} D \in SAlg$
23	22	salunid	$⊢ φ \to ⋃ (S ↾_{𝑡} D) \in (S ↾_{𝑡} D)$
24	18 23	eqeltrd	$⊢ φ \to D \in (S ↾_{𝑡} D)$
25	24	adantr	$⊢ (φ \land A = +∞) \to D \in (S ↾_{𝑡} D)$
26	15 25	eqeltrd	$⊢ (φ \land A = +∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
27		neqne	$⊢ \neg A = +∞ \to A \neq +∞$
28	27	adantl	$⊢ (φ \land \neg A = +∞) \to A \neq +∞$
29		breq2	$⊢ A = −∞ \to (F (x) < A \leftrightarrow F (x) < −∞)$
30	29	rabbidv	$⊢ A = −∞ \to \{x \in D \| F (x) < A\} = \{x \in D \| F (x) < −∞\}$
31	30	adantl	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < A\} = \{x \in D \| F (x) < −∞\}$
32	11	adantr	$⊢ (φ \land A = −∞) \to F : D ⟶ ℝ$
33	1 32	pimltmnf2	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < −∞\} = \emptyset$
34	31 33	eqtrd	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < A\} = \emptyset$
35	22	0sald	$⊢ φ \to \emptyset \in (S ↾_{𝑡} D)$
36	35	adantr	$⊢ (φ \land A = −∞) \to \emptyset \in (S ↾_{𝑡} D)$
37	34 36	eqeltrd	$⊢ (φ \land A = −∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
38	37	adantlr	$⊢ ((φ \land A \neq +∞) \land A = −∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
39		simpll	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to φ$
40	39 5	syl	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \in ℝ^{*}$
41		neqne	$⊢ \neg A = −∞ \to A \neq −∞$
42	41	adantl	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \neq −∞$
43		simplr	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \neq +∞$
44	40 42 43	xrred	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to A \in ℝ$
45	2	adantr	$⊢ (φ \land A \in ℝ) \to S \in SAlg$
46	3	adantr	$⊢ (φ \land A \in ℝ) \to F \in SMblFn (S)$
47		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
48	1 45 46 4 47	smfpreimaltf	$⊢ (φ \land A \in ℝ) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
49	39 44 48	syl2anc	$⊢ ((φ \land A \neq +∞) \land \neg A = −∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
50	38 49	pm2.61dan	$⊢ (φ \land A \neq +∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
51	28 50	syldan	$⊢ (φ \land \neg A = +∞) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
52	26 51	pm2.61dan	$⊢ φ \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfpimltxr

Proof