Theorem mbfmcnvima

Description: The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017)

	Ref	Expression
Hypotheses	mbfmf.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	mbfmf.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
	mbfmf.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
	mbfmcnvima.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
Assertion	mbfmcnvima	⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		mbfmf.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
2		mbfmf.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
3		mbfmf.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
4		mbfmcnvima.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
5		imaeq2	⊢ ( 𝑥 = 𝐴 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝐴 ) )
6	5	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ↔ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝑆 ) )
7	1 2	ismbfm	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) )
8	3 7	mpbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
9	8	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 )
10	6 9 4	rspcdva	⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝑆 )