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)

	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	7	adantl	$⊢ (φ \land A = −∞) \to \{x \in D \| A < F (x)\} = \{x \in D \| −∞ < F (x)\}$
9	1	nfdm	$⊢ \underline{Ⅎ} x dom F$
10	4 9	nfcxfr	$⊢ \underline{Ⅎ} x D$
11		nfcv	$⊢ \underline{Ⅎ} y D$
12		nfv	$⊢ Ⅎ y −∞ < F (x)$
13		nfcv	$⊢ \underline{Ⅎ} x −∞$
14		nfcv	$⊢ \underline{Ⅎ} x <$
15		nfcv	$⊢ \underline{Ⅎ} x y$
16	1 15	nffv	$⊢ \underline{Ⅎ} x F (y)$
17	13 14 16	nfbr	$⊢ Ⅎ x −∞ < F (y)$
18		fveq2	$⊢ x = y \to F (x) = F (y)$
19	18	breq2d	$⊢ x = y \to (−∞ < F (x) \leftrightarrow −∞ < F (y))$
20	10 11 12 17 19	cbvrabw	$⊢ \{x \in D \| −∞ < F (x)\} = \{y \in D \| −∞ < F (y)\}$
21	20	a1i	$⊢ φ \to \{x \in D \| −∞ < F (x)\} = \{y \in D \| −∞ < F (y)\}$
22		nfv	$⊢ Ⅎ y φ$
23	2 3 4	smff	$⊢ φ \to F : D ⟶ ℝ$
24	23	adantr	$⊢ (φ \land y \in D) \to F : D ⟶ ℝ$
25		simpr	$⊢ (φ \land y \in D) \to y \in D$
26	24 25	ffvelrnd	$⊢ (φ \land y \in D) \to F (y) \in ℝ$
27	22 26	pimgtmnf	$⊢ φ \to \{y \in D \| −∞ < F (y)\} = D$
28		eqidd	$⊢ φ \to D = D$
29	21 27 28	3eqtrd	$⊢ φ \to \{x \in D \| −∞ < F (x)\} = D$
30	29	adantr	$⊢ (φ \land A = −∞) \to \{x \in D \| −∞ < F (x)\} = D$
31	8 30	eqtrd	$⊢ (φ \land A = −∞) \to \{x \in D \| A < F (x)\} = D$
32	2 3 4	smfdmss	$⊢ φ \to D \subseteq ⋃ S$
33	2 32	restuni4	$⊢ φ \to ⋃ (S ↾_{𝑡} D) = D$
34	33	eqcomd	$⊢ φ \to D = ⋃ (S ↾_{𝑡} D)$
35	3	dmexd	$⊢ φ \to dom F \in V$
36	4 35	eqeltrid	$⊢ φ \to D \in V$
37		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
38	2 36 37	subsalsal	$⊢ φ \to S ↾_{𝑡} D \in SAlg$
39	38	salunid	$⊢ φ \to ⋃ (S ↾_{𝑡} D) \in (S ↾_{𝑡} D)$
40	34 39	eqeltrd	$⊢ φ \to D \in (S ↾_{𝑡} D)$
41	40	adantr	$⊢ (φ \land A = −∞) \to D \in (S ↾_{𝑡} D)$
42	31 41	eqeltrd	$⊢ (φ \land A = −∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
43		neqne	$⊢ \neg A = −∞ \to A \neq −∞$
44	43	adantl	$⊢ (φ \land \neg A = −∞) \to A \neq −∞$
45		breq1	$⊢ A = +∞ \to (A < F (x) \leftrightarrow +∞ < F (x))$
46	45	rabbidv	$⊢ A = +∞ \to \{x \in D \| A < F (x)\} = \{x \in D \| +∞ < F (x)\}$
47	46	adantl	$⊢ (φ \land A = +∞) \to \{x \in D \| A < F (x)\} = \{x \in D \| +∞ < F (x)\}$
48	1 23	pimgtpnf2	$⊢ φ \to \{x \in D \| +∞ < F (x)\} = \emptyset$
49	48	adantr	$⊢ (φ \land A = +∞) \to \{x \in D \| +∞ < F (x)\} = \emptyset$
50	47 49	eqtrd	$⊢ (φ \land A = +∞) \to \{x \in D \| A < F (x)\} = \emptyset$
51	38	0sald	$⊢ φ \to \emptyset \in (S ↾_{𝑡} D)$
52	51	adantr	$⊢ (φ \land A = +∞) \to \emptyset \in (S ↾_{𝑡} D)$
53	50 52	eqeltrd	$⊢ (φ \land A = +∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
54	53	adantlr	$⊢ ((φ \land A \neq −∞) \land A = +∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
55		simpll	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to φ$
56	55 5	syl	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \in ℝ^{*}$
57		simplr	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \neq −∞$
58		neqne	$⊢ \neg A = +∞ \to A \neq +∞$
59	58	adantl	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \neq +∞$
60	56 57 59	xrred	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to A \in ℝ$
61	2	adantr	$⊢ (φ \land A \in ℝ) \to S \in SAlg$
62	3	adantr	$⊢ (φ \land A \in ℝ) \to F \in SMblFn (S)$
63		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
64	1 61 62 4 63	smfpreimagtf	$⊢ (φ \land A \in ℝ) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
65	55 60 64	syl2anc	$⊢ ((φ \land A \neq −∞) \land \neg A = +∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
66	54 65	pm2.61dan	$⊢ (φ \land A \neq −∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
67	44 66	syldan	$⊢ (φ \land \neg A = −∞) \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
68	42 67	pm2.61dan	$⊢ φ \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfpimgtxr

Proof