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)

	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	7	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } )
9	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
10	4 9	nfcxfr	⊢ Ⅎ 𝑥 𝐷
11		nfcv	⊢ Ⅎ 𝑦 𝐷
12		nfv	⊢ Ⅎ 𝑦 -∞ < ( 𝐹 ‘ 𝑥 )
13		nfcv	⊢ Ⅎ 𝑥 -∞
14		nfcv	⊢ Ⅎ 𝑥 <
15		nfcv	⊢ Ⅎ 𝑥 𝑦
16	1 15	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
17	13 14 16	nfbr	⊢ Ⅎ 𝑥 -∞ < ( 𝐹 ‘ 𝑦 )
18		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
19	18	breq2d	⊢ ( 𝑥 = 𝑦 → ( -∞ < ( 𝐹 ‘ 𝑥 ) ↔ -∞ < ( 𝐹 ‘ 𝑦 ) ) )
20	10 11 12 17 19	cbvrabw	⊢ { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑦 ) }
21	20	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑦 ) } )
22		nfv	⊢ Ⅎ 𝑦 𝜑
23	2 3 4	smff	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐹 : 𝐷 ⟶ ℝ )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
26	24 25	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
27	22 26	pimgtmnf	⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑦 ) } = 𝐷 )
28		eqidd	⊢ ( 𝜑 → 𝐷 = 𝐷 )
29	21 27 28	3eqtrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } = 𝐷 )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } = 𝐷 )
31	8 30	eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = 𝐷 )
32	2 3 4	smfdmss	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
33	2 32	restuni4	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐷 ) = 𝐷 )
34	33	eqcomd	⊢ ( 𝜑 → 𝐷 = ∪ ( 𝑆 ↾t 𝐷 ) )
35	3	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
36	4 35	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ V )
37		eqid	⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
38	2 36 37	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
39	38	salunid	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) )
40	34 39	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
42	31 41	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
43		neqne	⊢ ( ¬ 𝐴 = -∞ → 𝐴 ≠ -∞ )
44	43	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ -∞ )
45		breq1	⊢ ( 𝐴 = +∞ → ( 𝐴 < ( 𝐹 ‘ 𝑥 ) ↔ +∞ < ( 𝐹 ‘ 𝑥 ) ) )
46	45	rabbidv	⊢ ( 𝐴 = +∞ → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } )
47	46	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } )
48	1 23	pimgtpnf2	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = ∅ )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = ∅ )
50	47 49	eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = ∅ )
51	38	0sald	⊢ ( 𝜑 → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
53	50 52	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
54	53	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
55		simpll	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝜑 )
56	55 5	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ∈ ℝ* )
57		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ≠ -∞ )
58		neqne	⊢ ( ¬ 𝐴 = +∞ → 𝐴 ≠ +∞ )
59	58	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ≠ +∞ )
60	56 57 59	xrred	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → 𝐴 ∈ ℝ )
61	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑆 ∈ SAlg )
62	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
63		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
64	1 61 62 4 63	smfpreimagtf	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
65	55 60 64	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
66	54 65	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
67	44 66	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
68	42 67	pm2.61dan	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )