Theorem isanmbfm

Description: The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017)

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

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		unieq	⊢ ( 𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆 )
7	6	oveq2d	⊢ ( 𝑠 = 𝑆 → ( ∪ 𝑡 ↑m ∪ 𝑠 ) = ( ∪ 𝑡 ↑m ∪ 𝑆 ) )
8	7	eleq2d	⊢ ( 𝑠 = 𝑆 → ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ↔ 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑆 ) ) )
9		eleq2	⊢ ( 𝑠 = 𝑆 → ( ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
10	9	ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
11	8 10	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) ↔ ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) )
12		unieq	⊢ ( 𝑡 = 𝑇 → ∪ 𝑡 = ∪ 𝑇 )
13	12	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ∪ 𝑡 ↑m ∪ 𝑆 ) = ( ∪ 𝑇 ↑m ∪ 𝑆 ) )
14	13	eleq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑆 ) ↔ 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ) )
15		raleq	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ↔ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
16	14 15	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) )
17	11 16	rspc2ev	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) → ∃ 𝑠 ∈ ∪ ran sigAlgebra ∃ 𝑡 ∈ ∪ ran sigAlgebra ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) )
18	1 2 5 17	syl3anc	⊢ ( 𝜑 → ∃ 𝑠 ∈ ∪ ran sigAlgebra ∃ 𝑡 ∈ ∪ ran sigAlgebra ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) )
19		elunirnmbfm	⊢ ( 𝐹 ∈ ∪ ran MblFnM ↔ ∃ 𝑠 ∈ ∪ ran sigAlgebra ∃ 𝑡 ∈ ∪ ran sigAlgebra ( 𝐹 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) )
20	18 19	sylibr	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )