Theorem ismbfm

Description: The predicate " F is a measurable function from the measurable space S to the measurable space T ". Cf. ismbf . (Contributed by Thierry Arnoux, 23-Jan-2017)

	Ref	Expression
Hypotheses	ismbfm.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	ismbfm.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
Assertion	ismbfm	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismbfm.1	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
2		ismbfm.2	⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra )
3		unieq	⊢ ( 𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆 )
4	3	oveq2d	⊢ ( 𝑠 = 𝑆 → ( ∪ 𝑡 ↑m ∪ 𝑠 ) = ( ∪ 𝑡 ↑m ∪ 𝑆 ) )
5		eleq2	⊢ ( 𝑠 = 𝑆 → ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑠 ↔ ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 ) )
6	5	ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑡 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 ) )
7	4 6	rabeqbidv	⊢ ( 𝑠 = 𝑆 → { 𝑓 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∣ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑠 } = { 𝑓 ∈ ( ∪ 𝑡 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } )
8		unieq	⊢ ( 𝑡 = 𝑇 → ∪ 𝑡 = ∪ 𝑇 )
9	8	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ∪ 𝑡 ↑m ∪ 𝑆 ) = ( ∪ 𝑇 ↑m ∪ 𝑆 ) )
10		raleq	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ 𝑡 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 ↔ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 ) )
11	9 10	rabeqbidv	⊢ ( 𝑡 = 𝑇 → { 𝑓 ∈ ( ∪ 𝑡 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } = { 𝑓 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } )
12		df-mbfm	⊢ MblFnM = ( 𝑠 ∈ ∪ ran sigAlgebra , 𝑡 ∈ ∪ ran sigAlgebra ↦ { 𝑓 ∈ ( ∪ 𝑡 ↑m ∪ 𝑠 ) ∣ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑠 } )
13		ovex	⊢ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∈ V
14	13	rabex	⊢ { 𝑓 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } ∈ V
15	7 11 12 14	ovmpo	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 MblFnM 𝑇 ) = { 𝑓 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } )
16	1 2 15	syl2anc	⊢ ( 𝜑 → ( 𝑆 MblFnM 𝑇 ) = { 𝑓 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } )
17	16	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } ) )
18		cnveq	⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
19	18	imaeq1d	⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑥 ) )
20	19	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
21	20	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 ↔ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
22	21	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∣ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝑆 } ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) )
23	17 22	bitrdi	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑m ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) )