Theorem 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	⊢ Ⅎ 𝑥 𝐹
	smfpimgtxr.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimgtxr.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimgtxr.d	⊢ 𝐷 = dom 𝐹
	smfpimgtxr.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
Assertion	smfpimgtxr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimgtxr.x	⊢ Ⅎ 𝑥 𝐹
2		smfpimgtxr.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpimgtxr.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
4		smfpimgtxr.d	⊢ 𝐷 = dom 𝐹
5		smfpimgtxr.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
6		breq1	⊢ ( 𝐴 = -∞ → ( 𝐴 < ( 𝐹 ‘ 𝑥 ) ↔ -∞ < ( 𝐹 ‘ 𝑥 ) ) )
7	6	rabbidv	⊢ ( 𝐴 = -∞ → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } )
8	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
9	4 8	nfcxfr	⊢ Ⅎ 𝑥 𝐷
10		nfcv	⊢ Ⅎ 𝑦 𝐷
11		nfv	⊢ Ⅎ 𝑦 -∞ < ( 𝐹 ‘ 𝑥 )
12		nfcv	⊢ Ⅎ 𝑥 -∞
13		nfcv	⊢ Ⅎ 𝑥 <
14		nfcv	⊢ Ⅎ 𝑥 𝑦
15	1 14	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
16	12 13 15	nfbr	⊢ Ⅎ 𝑥 -∞ < ( 𝐹 ‘ 𝑦 )
17		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
18	17	breq2d	⊢ ( 𝑥 = 𝑦 → ( -∞ < ( 𝐹 ‘ 𝑥 ) ↔ -∞ < ( 𝐹 ‘ 𝑦 ) ) )
19	9 10 11 16 18	cbvrabw	⊢ { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑦 ) }
20		nfv	⊢ Ⅎ 𝑦 𝜑
21	2 3 4	smff	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
22	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
23	20 22	pimgtmnf	⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑦 ) } = 𝐷 )
24	19 23	eqtrid	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } = 𝐷 )
25	7 24	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = 𝐷 )
26	2 3 4	smfdmss	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
27	2 26	subsaluni	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
29	25 28	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
30		breq1	⊢ ( 𝐴 = +∞ → ( 𝐴 < ( 𝐹 ‘ 𝑥 ) ↔ +∞ < ( 𝐹 ‘ 𝑥 ) ) )
31	30	rabbidv	⊢ ( 𝐴 = +∞ → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } )
32	1 9 21	pimgtpnf2f	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = ∅ )
33	31 32	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = ∅ )
34	3	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
35	4 34	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ V )
36		eqid	⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
37	2 35 36	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
38	37	0sald	⊢ ( 𝜑 → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
40	33 39	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
41	40	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
42		simpll	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝜑 )
43	42 5	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ∈ ℝ* )
44		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ≠ -∞ )
45		neqne	⊢ ( ¬ 𝐴 = +∞ → 𝐴 ≠ +∞ )
46	45	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ≠ +∞ )
47	43 44 46	xrred	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ∈ ℝ )
48	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑆 ∈ SAlg )
49	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
50		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
51	1 48 49 4 50	smfpreimagtf	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
52	42 47 51	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
53	41 52	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
54	29 53	pm2.61dane	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )