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 
|- ( ph -> K e. _V )
imambfm.2 
|- ( ph -> S e. U. ran sigAlgebra )
imambfm.3 
|- ( ph -> T = ( sigaGen ` K ) )
Assertion imambfm 
|- ( ph -> ( F e. ( S MblFnM T ) <-> ( F : U. S --> U. T /\ A. a e. K ( `' F " a ) e. S ) ) )

Proof

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