Theorem mbfmf

Description: A measurable function as a function with domain and codomain. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypotheses	mbfmf.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	mbfmf.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
	mbfmf.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
Assertion	mbfmf	⊢ ( 𝜑 → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		mbfmf.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
2		mbfmf.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
3		mbfmf.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
4	1 2	ismbfm	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) )
5	3 4	mpbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
6	5	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) )
7		elmapi	⊢ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
8	6 7	syl	⊢ ( 𝜑 → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )