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	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	ismbfm.2	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
Assertion	ismbfm	$$⊢\phi \to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow \left(F\in \left({\bigcup T}^{\bigcup S}\right)\wedge \forall x\in T{F}^{-1}\left[x\right]\in S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismbfm.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
2		ismbfm.2	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
3		unieq	$$⊢s=S\to \bigcup s=\bigcup S$$
4	3	oveq2d	$$⊢s=S\to {\bigcup t}^{\bigcup s}={\bigcup t}^{\bigcup S}$$
5		eleq2	$$⊢s=S\to \left(f^{-1}\left[x\right]\in s\leftrightarrow f^{-1}\left[x\right]\in S\right)$$
6	5	ralbidv	$$⊢s=S\to \left(\forall x\in t{f}^{-1}\left[x\right]\in s\leftrightarrow \forall x\in t{f}^{-1}\left[x\right]\in S\right)$$
7	4 6	rabeqbidv	$$⊢s=S\to \left\{f\in \left({\bigcup t}^{\bigcup s}\right)|\forall x\in t{f}^{-1}\left[x\right]\in s\right\}=\left\{f\in \left({\bigcup t}^{\bigcup S}\right)|\forall x\in t{f}^{-1}\left[x\right]\in S\right\}$$
8		unieq	$$⊢t=T\to \bigcup t=\bigcup T$$
9	8	oveq1d	$$⊢t=T\to {\bigcup t}^{\bigcup S}={\bigcup T}^{\bigcup S}$$
10		raleq	$$⊢t=T\to \left(\forall x\in t{f}^{-1}\left[x\right]\in S\leftrightarrow \forall x\in T{f}^{-1}\left[x\right]\in S\right)$$
11	9 10	rabeqbidv	$$⊢t=T\to \left\{f\in \left({\bigcup t}^{\bigcup S}\right)|\forall x\in t{f}^{-1}\left[x\right]\in S\right\}=\left\{f\in \left({\bigcup T}^{\bigcup S}\right)|\forall x\in T{f}^{-1}\left[x\right]\in S\right\}$$
12		df-mbfm	$$⊢{\mathrm{MblFn}}_{\mu }=\left(s\in \bigcup \mathrm{ran}\mathrm{sigAlgebra},t\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}⟼\left\{f\in \left({\bigcup t}^{\bigcup s}\right)|\forall x\in t{f}^{-1}\left[x\right]\in s\right\}\right)$$
13		ovex	$$⊢{\bigcup T}^{\bigcup S}\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{f\in \left({\bigcup T}^{\bigcup S}\right)|\forall x\in T{f}^{-1}\left[x\right]\in S\right\}\in \mathrm{V}$$
15	7 11 12 14	ovmpo	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to S{\mathrm{MblFn}}_{\mu }T=\left\{f\in \left({\bigcup T}^{\bigcup S}\right)|\forall x\in T{f}^{-1}\left[x\right]\in S\right\}$$
16	1 2 15	syl2anc	$$⊢\phi \to S{\mathrm{MblFn}}_{\mu }T=\left\{f\in \left({\bigcup T}^{\bigcup S}\right)|\forall x\in T{f}^{-1}\left[x\right]\in S\right\}$$
17	16	eleq2d	$$⊢\phi \to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow F\in \left\{f\in \left({\bigcup T}^{\bigcup S}\right)|\forall x\in T{f}^{-1}\left[x\right]\in S\right\}\right)$$
18		cnveq	$$⊢f=F\to f^{-1}=F^{-1}$$
19	18	imaeq1d	$$⊢f=F\to f^{-1}\left[x\right]=F^{-1}\left[x\right]$$
20	19	eleq1d	$$⊢f=F\to \left(f^{-1}\left[x\right]\in S\leftrightarrow F^{-1}\left[x\right]\in S\right)$$
21	20	ralbidv	$$⊢f=F\to \left(\forall x\in T{f}^{-1}\left[x\right]\in S\leftrightarrow \forall x\in T{F}^{-1}\left[x\right]\in S\right)$$
22	21	elrab	$$⊢F\in \left\{f\in \left({\bigcup T}^{\bigcup S}\right)|\forall x\in T{f}^{-1}\left[x\right]\in S\right\}\leftrightarrow \left(F\in \left({\bigcup T}^{\bigcup S}\right)\wedge \forall x\in T{F}^{-1}\left[x\right]\in S\right)$$
23	17 22	bitrdi	$$⊢\phi \to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow \left(F\in \left({\bigcup T}^{\bigcup S}\right)\wedge \forall x\in T{F}^{-1}\left[x\right]\in S\right)\right)$$