Theorem mbfmfun

Description: A measurable function is a function. (Contributed by Thierry Arnoux, 24-Jan-2017)

	Ref	Expression
Hypothesis	mbfmfun.1	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )
Assertion	mbfmfun	⊢ ( 𝜑 → Fun 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		mbfmfun.1	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )
2		elunirnmbfm	⊢ ( 𝐹 ∈ ∪ ran MblFnM ↔ ∃ 𝑠 ∈ ∪ ran sigAlgebra ∃ 𝑡 ∈ ∪ ran sigAlgebra ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) )
3	2	biimpi	⊢ ( 𝐹 ∈ ∪ ran MblFnM → ∃ 𝑠 ∈ ∪ ran sigAlgebra ∃ 𝑡 ∈ ∪ ran sigAlgebra ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) )
4		elmapfun	⊢ ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) → Fun 𝐹 )
5	4	adantr	⊢ ( ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) → Fun 𝐹 )
6	5	rexlimivw	⊢ ( ∃ 𝑡 ∈ ∪ ran sigAlgebra ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) → Fun 𝐹 )
7	6	rexlimivw	⊢ ( ∃ 𝑠 ∈ ∪ ran sigAlgebra ∃ 𝑡 ∈ ∪ ran sigAlgebra ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) → Fun 𝐹 )
8	1 3 7	3syl	⊢ ( 𝜑 → Fun 𝐹 )