Theorem imambfm

Description: If the sigma-algebra in the range of a given function is generated by a collection of basic sets K , then to check the measurability of that function, we need only consider inverse images of basic sets a . (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Hypotheses	imambfm.1	$$⊢\phi \to K\in \mathrm{V}$$
	imambfm.2	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	imambfm.3	$$⊢\phi \to T=𝛔\left(K\right)$$
Assertion	imambfm	$$⊢\phi \to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		imambfm.1	$$⊢\phi \to K\in \mathrm{V}$$
2		imambfm.2	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
3		imambfm.3	$$⊢\phi \to T=𝛔\left(K\right)$$
4	2	adantr	$$⊢\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
5	1	sgsiga	$$⊢\phi \to 𝛔\left(K\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
6	3 5	eqeltrd	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
7	6	adantr	$$⊢\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
8		simpr	$$⊢\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
9	4 7 8	mbfmf	$$⊢\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\to F:\bigcup S⟶\bigcup T$$
10	2	ad2antrr	$$⊢\left(\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\wedge a\in K\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
11	6	ad2antrr	$$⊢\left(\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\wedge a\in K\right)\to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
12		simplr	$$⊢\left(\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\wedge a\in K\right)\to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
13		sssigagen	$$⊢K\in \mathrm{V}\to K\subseteq 𝛔\left(K\right)$$
14	1 13	syl	$$⊢\phi \to K\subseteq 𝛔\left(K\right)$$
15	14 3	sseqtrrd	$$⊢\phi \to K\subseteq T$$
16	15	ad2antrr	$$⊢\left(\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\wedge a\in K\right)\to K\subseteq T$$
17		simpr	$$⊢\left(\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\wedge a\in K\right)\to a\in K$$
18	16 17	sseldd	$$⊢\left(\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\wedge a\in K\right)\to a\in T$$
19	10 11 12 18	mbfmcnvima	$$⊢\left(\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\wedge a\in K\right)\to F^{-1}\left[a\right]\in S$$
20	19	ralrimiva	$$⊢\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\to \forall a\in K{F}^{-1}\left[a\right]\in S$$
21	9 20	jca	$$⊢\left(\phi \wedge F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\right)\to \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)$$
22		unielsiga	$$⊢T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup T\in T$$
23	6 22	syl	$$⊢\phi \to \bigcup T\in T$$
24	23	adantr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \bigcup T\in T$$
25		unielsiga	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup S\in S$$
26	2 25	syl	$$⊢\phi \to \bigcup S\in S$$
27	26	adantr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \bigcup S\in S$$
28		simprl	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to F:\bigcup S⟶\bigcup T$$
29		elmapg	$$⊢\left(\bigcup T\in T\wedge \bigcup S\in S\right)\to \left(F\in \left({\bigcup T}^{\bigcup S}\right)\leftrightarrow F:\bigcup S⟶\bigcup T\right)$$
30	29	biimpar	$$⊢\left(\left(\bigcup T\in T\wedge \bigcup S\in S\right)\wedge F:\bigcup S⟶\bigcup T\right)\to F\in \left({\bigcup T}^{\bigcup S}\right)$$
31	24 27 28 30	syl21anc	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to F\in \left({\bigcup T}^{\bigcup S}\right)$$
32	3	adantr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to T=𝛔\left(K\right)$$
33		simpl	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \phi$$
34		ssrab2	$$⊢\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq T$$
35		pwuni	$$⊢T\subseteq 𝒫\bigcup T$$
36	34 35	sstri	$$⊢\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq 𝒫\bigcup T$$
37	36	a1i	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq 𝒫\bigcup T$$
38		fimacnv	$$⊢F:\bigcup S⟶\bigcup T\to F^{-1}\left[\bigcup T\right]=\bigcup S$$
39	38	ad2antrl	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to F^{-1}\left[\bigcup T\right]=\bigcup S$$
40	39 27	eqeltrd	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to F^{-1}\left[\bigcup T\right]\in S$$
41		imaeq2	$$⊢a=\bigcup T\to F^{-1}\left[a\right]=F^{-1}\left[\bigcup T\right]$$
42	41	eleq1d	$$⊢a=\bigcup T\to \left(F^{-1}\left[a\right]\in S\leftrightarrow F^{-1}\left[\bigcup T\right]\in S\right)$$
43	42	elrab	$$⊢\bigcup T\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\leftrightarrow \left(\bigcup T\in T\wedge F^{-1}\left[\bigcup T\right]\in S\right)$$
44	24 40 43	sylanbrc	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \bigcup T\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
45	6	ad2antrr	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
46	45 22	syl	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to \bigcup T\in T$$
47		elrabi	$$⊢x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\to x\in T$$
48	47	adantl	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to x\in T$$
49		difelsiga	$$⊢\left(T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup T\in T\wedge x\in T\right)\to \bigcup T\setminus x\in T$$
50	45 46 48 49	syl3anc	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to \bigcup T\setminus x\in T$$
51		simplrl	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to F:\bigcup S⟶\bigcup T$$
52		ffun	$$⊢F:\bigcup S⟶\bigcup T\to \mathrm{Fun}F$$
53		difpreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[\bigcup T\setminus x\right]=F^{-1}\left[\bigcup T\right]\setminus F^{-1}\left[x\right]$$
54	51 52 53	3syl	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to F^{-1}\left[\bigcup T\setminus x\right]=F^{-1}\left[\bigcup T\right]\setminus F^{-1}\left[x\right]$$
55	39	difeq1d	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to F^{-1}\left[\bigcup T\right]\setminus F^{-1}\left[x\right]=\bigcup S\setminus F^{-1}\left[x\right]$$
56	55	adantr	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to F^{-1}\left[\bigcup T\right]\setminus F^{-1}\left[x\right]=\bigcup S\setminus F^{-1}\left[x\right]$$
57	2	ad2antrr	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
58	57 25	syl	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to \bigcup S\in S$$
59		imaeq2	$$⊢a=x\to F^{-1}\left[a\right]=F^{-1}\left[x\right]$$
60	59	eleq1d	$$⊢a=x\to \left(F^{-1}\left[a\right]\in S\leftrightarrow F^{-1}\left[x\right]\in S\right)$$
61	60	elrab	$$⊢x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\leftrightarrow \left(x\in T\wedge F^{-1}\left[x\right]\in S\right)$$
62	61	simprbi	$$⊢x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\to F^{-1}\left[x\right]\in S$$
63	62	adantl	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to F^{-1}\left[x\right]\in S$$
64		difelsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup S\in S\wedge F^{-1}\left[x\right]\in S\right)\to \bigcup S\setminus F^{-1}\left[x\right]\in S$$
65	57 58 63 64	syl3anc	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to \bigcup S\setminus F^{-1}\left[x\right]\in S$$
66	56 65	eqeltrd	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to F^{-1}\left[\bigcup T\right]\setminus F^{-1}\left[x\right]\in S$$
67	54 66	eqeltrd	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to F^{-1}\left[\bigcup T\setminus x\right]\in S$$
68		imaeq2	$$⊢a=\bigcup T\setminus x\to F^{-1}\left[a\right]=F^{-1}\left[\bigcup T\setminus x\right]$$
69	68	eleq1d	$$⊢a=\bigcup T\setminus x\to \left(F^{-1}\left[a\right]\in S\leftrightarrow F^{-1}\left[\bigcup T\setminus x\right]\in S\right)$$
70	69	elrab	$$⊢\bigcup T\setminus x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\leftrightarrow \left(\bigcup T\setminus x\in T\wedge F^{-1}\left[\bigcup T\setminus x\right]\in S\right)$$
71	50 67 70	sylanbrc	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to \bigcup T\setminus x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
72	71	ralrimiva	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \forall x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\bigcup T\setminus x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
73	6	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
74	34	sspwi	$$⊢𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq 𝒫T$$
75	74	sseli	$$⊢x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\to x\in 𝒫T$$
76	75	ad2antlr	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to x\in 𝒫T$$
77		simpr	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to x\preccurlyeq \mathrm{\omega }$$
78		sigaclcu	$$⊢\left(T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge x\in 𝒫T\wedge x\preccurlyeq \mathrm{\omega }\right)\to \bigcup x\in T$$
79	73 76 77 78	syl3anc	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to \bigcup x\in T$$
80		simpllr	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)$$
81	80	simpld	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to F:\bigcup S⟶\bigcup T$$
82		unipreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[\bigcup x\right]=\bigcup _{y\in x}{F}^{-1}\left[y\right]$$
83	81 52 82	3syl	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to F^{-1}\left[\bigcup x\right]=\bigcup _{y\in x}{F}^{-1}\left[y\right]$$
84	2	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
85		simpr	$$⊢\left(\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\wedge y\in x\right)\to y\in x$$
86		simpllr	$$⊢\left(\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\wedge y\in x\right)\to x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
87		elelpwi	$$⊢\left(y\in x\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to y\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
88	85 86 87	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\wedge y\in x\right)\to y\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
89		imaeq2	$$⊢a=y\to F^{-1}\left[a\right]=F^{-1}\left[y\right]$$
90	89	eleq1d	$$⊢a=y\to \left(F^{-1}\left[a\right]\in S\leftrightarrow F^{-1}\left[y\right]\in S\right)$$
91	90	elrab	$$⊢y\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\leftrightarrow \left(y\in T\wedge F^{-1}\left[y\right]\in S\right)$$
92	91	simprbi	$$⊢y\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\to F^{-1}\left[y\right]\in S$$
93	88 92	syl	$$⊢\left(\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\wedge y\in x\right)\to F^{-1}\left[y\right]\in S$$
94	93	ralrimiva	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to \forall y\in x{F}^{-1}\left[y\right]\in S$$
95		nfcv	$$⊢\underset{\_}{Ⅎ}yx$$
96	95	sigaclcuni	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall y\in x{F}^{-1}\left[y\right]\in S\wedge x\preccurlyeq \mathrm{\omega }\right)\to \bigcup _{y\in x}{F}^{-1}\left[y\right]\in S$$
97	84 94 77 96	syl3anc	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to \bigcup _{y\in x}{F}^{-1}\left[y\right]\in S$$
98	83 97	eqeltrd	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to F^{-1}\left[\bigcup x\right]\in S$$
99		imaeq2	$$⊢a=\bigcup x\to F^{-1}\left[a\right]=F^{-1}\left[\bigcup x\right]$$
100	99	eleq1d	$$⊢a=\bigcup x\to \left(F^{-1}\left[a\right]\in S\leftrightarrow F^{-1}\left[\bigcup x\right]\in S\right)$$
101	100	elrab	$$⊢\bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\leftrightarrow \left(\bigcup x\in T\wedge F^{-1}\left[\bigcup x\right]\in S\right)$$
102	79 98 101	sylanbrc	$$⊢\left(\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\wedge x\preccurlyeq \mathrm{\omega }\right)\to \bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
103	102	ex	$$⊢\left(\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\wedge x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to \left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)$$
104	103	ralrimiva	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \forall x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)$$
105	44 72 104	3jca	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \left(\bigcup T\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\bigcup T\setminus x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\right)$$
106		rabexg	$$⊢T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{V}$$
107		issiga	$$⊢\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{V}\to \left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup T\right)\leftrightarrow \left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq 𝒫\bigcup T\wedge \left(\bigcup T\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\bigcup T\setminus x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\right)\right)\right)$$
108	6 106 107	3syl	$$⊢\phi \to \left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup T\right)\leftrightarrow \left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq 𝒫\bigcup T\wedge \left(\bigcup T\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\bigcup T\setminus x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\right)\right)\right)$$
109	108	biimpar	$$⊢\left(\phi \wedge \left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq 𝒫\bigcup T\wedge \left(\bigcup T\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\bigcup T\setminus x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\wedge \forall x\in 𝒫\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\right)\right)\right)\to \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup T\right)$$
110	33 37 105 109	syl12anc	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup T\right)$$
111	3	unieqd	$$⊢\phi \to \bigcup T=\bigcup 𝛔\left(K\right)$$
112		unisg	$$⊢K\in \mathrm{V}\to \bigcup 𝛔\left(K\right)=\bigcup K$$
113	1 112	syl	$$⊢\phi \to \bigcup 𝛔\left(K\right)=\bigcup K$$
114	111 113	eqtrd	$$⊢\phi \to \bigcup T=\bigcup K$$
115	114	fveq2d	$$⊢\phi \to \mathrm{sigAlgebra}\left(\bigcup T\right)=\mathrm{sigAlgebra}\left(\bigcup K\right)$$
116	115	eleq2d	$$⊢\phi \to \left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup T\right)\leftrightarrow \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup K\right)\right)$$
117	116	adantr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup T\right)\leftrightarrow \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup K\right)\right)$$
118	110 117	mpbid	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup K\right)$$
119	15	adantr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to K\subseteq T$$
120		simprr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \forall a\in K{F}^{-1}\left[a\right]\in S$$
121		ssrab	$$⊢K\subseteq \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\leftrightarrow \left(K\subseteq T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)$$
122	119 120 121	sylanbrc	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to K\subseteq \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
123		sigagenss	$$⊢\left(\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\in \mathrm{sigAlgebra}\left(\bigcup K\right)\wedge K\subseteq \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\right)\to 𝛔\left(K\right)\subseteq \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
124	118 122 123	syl2anc	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to 𝛔\left(K\right)\subseteq \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
125	32 124	eqsstrd	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to T\subseteq \left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
126	34	a1i	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \left\{a\in T|F^{-1}\left[a\right]\in S\right\}\subseteq T$$
127	125 126	eqssd	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to T=\left\{a\in T|F^{-1}\left[a\right]\in S\right\}$$
128		rabid2	$$⊢T=\left\{a\in T|F^{-1}\left[a\right]\in S\right\}\leftrightarrow \forall a\in T{F}^{-1}\left[a\right]\in S$$
129	127 128	sylib	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \forall a\in T{F}^{-1}\left[a\right]\in S$$
130	2	adantr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
131	6	adantr	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
132	130 131	ismbfm	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow \left(F\in \left({\bigcup T}^{\bigcup S}\right)\wedge \forall a\in T{F}^{-1}\left[a\right]\in S\right)\right)$$
133	31 129 132	mpbir2and	$$⊢\left(\phi \wedge \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)\to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
134	21 133	impbida	$$⊢\phi \to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow \left(F:\bigcup S⟶\bigcup T\wedge \forall a\in K{F}^{-1}\left[a\right]\in S\right)\right)$$