# Metamath Proof Explorer

## 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)↔\left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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)↔{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}↔{{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\}↔\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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}↔{{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\}↔\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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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}↔{{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\}↔\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}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{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\}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}{{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 sspwb ${⊢}\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\subseteq {T}↔𝒫\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\subseteq 𝒫{T}$
75 34 74 mpbi ${⊢}𝒫\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\subseteq 𝒫{T}$
76 75 sseli ${⊢}{x}\in 𝒫\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\to {x}\in 𝒫{T}$
77 76 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
78 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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 }$
79 sigaclcu ${⊢}\left({T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {x}\in 𝒫{T}\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to \bigcup {x}\in {T}$
80 73 77 78 79 syl3anc ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
81 simpllr ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)$
82 81 simpld ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
83 unipreima ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[\bigcup {x}\right]=\bigcup _{{y}\in {x}}{{F}}^{-1}\left[{y}\right]$
84 82 52 83 3syl ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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]$
85 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
86 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
87 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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\}$
88 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\}$
89 86 87 88 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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\}$
90 imaeq2 ${⊢}{a}={y}\to {{F}}^{-1}\left[{a}\right]={{F}}^{-1}\left[{y}\right]$
91 90 eleq1d ${⊢}{a}={y}\to \left({{F}}^{-1}\left[{a}\right]\in {S}↔{{F}}^{-1}\left[{y}\right]\in {S}\right)$
92 91 elrab ${⊢}{y}\in \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}↔\left({y}\in {T}\wedge {{F}}^{-1}\left[{y}\right]\in {S}\right)$
93 92 simprbi ${⊢}{y}\in \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\to {{F}}^{-1}\left[{y}\right]\in {S}$
94 89 93 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
95 94 ralrimiva ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {S}$
96 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{x}$
97 96 sigaclcuni ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{{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}$
98 85 95 78 97 syl3anc ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
99 84 98 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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}$
100 imaeq2 ${⊢}{a}=\bigcup {x}\to {{F}}^{-1}\left[{a}\right]={{F}}^{-1}\left[\bigcup {x}\right]$
101 100 eleq1d ${⊢}{a}=\bigcup {x}\to \left({{F}}^{-1}\left[{a}\right]\in {S}↔{{F}}^{-1}\left[\bigcup {x}\right]\in {S}\right)$
102 101 elrab ${⊢}\bigcup {x}\in \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}↔\left(\bigcup {x}\in {T}\wedge {{F}}^{-1}\left[\bigcup {x}\right]\in {S}\right)$
103 80 99 102 sylanbrc ${⊢}\left(\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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\}$
104 103 ex ${⊢}\left(\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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)$
105 104 ralrimiva ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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\}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\right)$
106 44 72 105 3jca ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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\}\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\right)\right)$
107 rabexg ${⊢}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\in \mathrm{V}$
108 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)↔\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\}\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}\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 6 107 108 3syl ${⊢}{\phi }\to \left(\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\in \mathrm{sigAlgebra}\left(\bigcup {T}\right)↔\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\}\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}\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)$
110 109 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\}\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}\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)$
111 33 37 106 110 syl12anc ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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)$
112 3 unieqd ${⊢}{\phi }\to \bigcup {T}=\bigcup 𝛔\left({K}\right)$
113 unisg ${⊢}{K}\in \mathrm{V}\to \bigcup 𝛔\left({K}\right)=\bigcup {K}$
114 1 113 syl ${⊢}{\phi }\to \bigcup 𝛔\left({K}\right)=\bigcup {K}$
115 112 114 eqtrd ${⊢}{\phi }\to \bigcup {T}=\bigcup {K}$
116 115 fveq2d ${⊢}{\phi }\to \mathrm{sigAlgebra}\left(\bigcup {T}\right)=\mathrm{sigAlgebra}\left(\bigcup {K}\right)$
117 116 eleq2d ${⊢}{\phi }\to \left(\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\in \mathrm{sigAlgebra}\left(\bigcup {T}\right)↔\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\in \mathrm{sigAlgebra}\left(\bigcup {K}\right)\right)$
118 117 adantr ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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)↔\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\in \mathrm{sigAlgebra}\left(\bigcup {K}\right)\right)$
119 111 118 mpbid ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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)$
120 15 adantr ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to {K}\subseteq {T}$
121 simprr ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}$
122 ssrab ${⊢}{K}\subseteq \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}↔\left({K}\subseteq {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)$
123 120 121 122 sylanbrc ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to {K}\subseteq \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}$
124 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\}$
125 119 123 124 syl2anc ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{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\}$
126 32 125 eqsstrd ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to {T}\subseteq \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}$
127 34 a1i ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to \left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}\subseteq {T}$
128 126 127 eqssd ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to {T}=\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}$
129 rabid2 ${⊢}{T}=\left\{{a}\in {T}|{{F}}^{-1}\left[{a}\right]\in {S}\right\}↔\forall {a}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}$
130 128 129 sylib ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to \forall {a}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}$
131 2 adantr ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
132 6 adantr ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
133 131 132 ismbfm ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to \left({F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)↔\left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\wedge \forall {a}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)$
134 31 130 133 mpbir2and ${⊢}\left({\phi }\wedge \left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)\to {F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$
135 21 134 impbida ${⊢}{\phi }\to \left({F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)↔\left({F}:\bigcup {S}⟶\bigcup {T}\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{a}\right]\in {S}\right)\right)$