Theorem smfpreimagtf

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

Proof

Step	Hyp	Ref	Expression
1		smfpreimagtf.x	⊢ Ⅎ 𝑥 𝐹
2		smfpreimagtf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpreimagtf.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
4		smfpreimagtf.d	⊢ 𝐷 = dom 𝐹
5		smfpreimagtf.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
7	4 6	nfcxfr	⊢ Ⅎ 𝑥 𝐷
8		nfcv	⊢ Ⅎ 𝑦 𝐷
9		nfv	⊢ Ⅎ 𝑦 𝐴 < ( 𝐹 ‘ 𝑥 )
10		nfcv	⊢ Ⅎ 𝑥 𝐴
11		nfcv	⊢ Ⅎ 𝑥 <
12		nfcv	⊢ Ⅎ 𝑥 𝑦
13	1 12	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
14	10 11 13	nfbr	⊢ Ⅎ 𝑥 𝐴 < ( 𝐹 ‘ 𝑦 )
15		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
16	15	breq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 < ( 𝐹 ‘ 𝑥 ) ↔ 𝐴 < ( 𝐹 ‘ 𝑦 ) ) )
17	7 8 9 14 16	cbvrabw	⊢ { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑦 ) }
18	17	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑦 ) } )
19	2 3 4 5	smfpreimagt	⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
20	18 19	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )