Metamath Proof Explorer

Theorem mbfresfi

Description: Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018)

Ref Expression
Hypotheses mbfresfi.1 
|- ( ph -> F : A --> CC )
mbfresfi.2 
|- ( ph -> S e. Fin )
mbfresfi.3 
|- ( ph -> A. s e. S ( F |` s ) e. MblFn )
mbfresfi.4 
|- ( ph -> U. S = A )
Assertion mbfresfi 
|- ( ph -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfresfi.1 
 |-  ( ph -> F : A --> CC )
2 mbfresfi.2 
 |-  ( ph -> S e. Fin )
3 mbfresfi.3 
 |-  ( ph -> A. s e. S ( F |` s ) e. MblFn )
4 mbfresfi.4 
 |-  ( ph -> U. S = A )
5 2 uniexd 
 |-  ( ph -> U. S e. _V )
6 4 5 eqeltrrd 
 |-  ( ph -> A e. _V )
7 fex 
 |-  ( ( F : A --> CC /\ A e. _V ) -> F e. _V )
8 7 ex 
 |-  ( F : A --> CC -> ( A e. _V -> F e. _V ) )
9 1 8 syl 
 |-  ( ph -> ( A e. _V -> F e. _V ) )
10 6 9 jcai 
 |-  ( ph -> ( A e. _V /\ F e. _V ) )
11 feq2 
 |-  ( a = A -> ( f : a --> CC <-> f : A --> CC ) )
12 11 anbi1d 
 |-  ( a = A -> ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) <-> ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) ) )
13 eqeq2 
 |-  ( a = A -> ( U. S = a <-> U. S = A ) )
14 12 13 anbi12d 
 |-  ( a = A -> ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) <-> ( ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = A ) ) )
15 14 imbi1d 
 |-  ( a = A -> ( ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) <-> ( ( ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = A ) -> f e. MblFn ) ) )
16 15 imbi2d 
 |-  ( a = A -> ( ( ph -> ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) ) <-> ( ph -> ( ( ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = A ) -> f e. MblFn ) ) ) )
17 feq1 
 |-  ( f = F -> ( f : A --> CC <-> F : A --> CC ) )
18 reseq1 
 |-  ( f = F -> ( f |` s ) = ( F |` s ) )
19 18 eleq1d 
 |-  ( f = F -> ( ( f |` s ) e. MblFn <-> ( F |` s ) e. MblFn ) )
20 19 ralbidv 
 |-  ( f = F -> ( A. s e. S ( f |` s ) e. MblFn <-> A. s e. S ( F |` s ) e. MblFn ) )
21 17 20 anbi12d 
 |-  ( f = F -> ( ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) <-> ( F : A --> CC /\ A. s e. S ( F |` s ) e. MblFn ) ) )
22 21 anbi1d 
 |-  ( f = F -> ( ( ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = A ) <-> ( ( F : A --> CC /\ A. s e. S ( F |` s ) e. MblFn ) /\ U. S = A ) ) )
23 eleq1 
 |-  ( f = F -> ( f e. MblFn <-> F e. MblFn ) )
24 22 23 imbi12d 
 |-  ( f = F -> ( ( ( ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = A ) -> f e. MblFn ) <-> ( ( ( F : A --> CC /\ A. s e. S ( F |` s ) e. MblFn ) /\ U. S = A ) -> F e. MblFn ) ) )
25 24 imbi2d 
 |-  ( f = F -> ( ( ph -> ( ( ( f : A --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = A ) -> f e. MblFn ) ) <-> ( ph -> ( ( ( F : A --> CC /\ A. s e. S ( F |` s ) e. MblFn ) /\ U. S = A ) -> F e. MblFn ) ) ) )
26 rzal 
 |-  ( r = (/) -> A. s e. r ( f |` s ) e. MblFn )
27 26 biantrud 
 |-  ( r = (/) -> ( f : a --> CC <-> ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) ) )
28 27 bicomd 
 |-  ( r = (/) -> ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) <-> f : a --> CC ) )
29 unieq 
 |-  ( r = (/) -> U. r = U. (/) )
30 uni0 
 |-  U. (/) = (/)
31 29 30 eqtrdi 
 |-  ( r = (/) -> U. r = (/) )
32 31 eqeq1d 
 |-  ( r = (/) -> ( U. r = a <-> (/) = a ) )
33 28 32 anbi12d 
 |-  ( r = (/) -> ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) <-> ( f : a --> CC /\ (/) = a ) ) )
34 33 imbi1d 
 |-  ( r = (/) -> ( ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> ( ( f : a --> CC /\ (/) = a ) -> f e. MblFn ) ) )
35 34 2albidv 
 |-  ( r = (/) -> ( A. f A. a ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> A. f A. a ( ( f : a --> CC /\ (/) = a ) -> f e. MblFn ) ) )
36 raleq 
 |-  ( r = t -> ( A. s e. r ( f |` s ) e. MblFn <-> A. s e. t ( f |` s ) e. MblFn ) )
37 36 anbi2d 
 |-  ( r = t -> ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) <-> ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) ) )
38 unieq 
 |-  ( r = t -> U. r = U. t )
39 38 eqeq1d 
 |-  ( r = t -> ( U. r = a <-> U. t = a ) )
40 37 39 anbi12d 
 |-  ( r = t -> ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) <-> ( ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) /\ U. t = a ) ) )
41 40 imbi1d 
 |-  ( r = t -> ( ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> ( ( ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) /\ U. t = a ) -> f e. MblFn ) ) )
42 41 2albidv 
 |-  ( r = t -> ( A. f A. a ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> A. f A. a ( ( ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) /\ U. t = a ) -> f e. MblFn ) ) )
43 simpl 
 |-  ( ( f = g /\ a = b ) -> f = g )
44 simpr 
 |-  ( ( f = g /\ a = b ) -> a = b )
45 43 44 feq12d 
 |-  ( ( f = g /\ a = b ) -> ( f : a --> CC <-> g : b --> CC ) )
46 reseq1 
 |-  ( f = g -> ( f |` s ) = ( g |` s ) )
47 46 adantr 
 |-  ( ( f = g /\ a = b ) -> ( f |` s ) = ( g |` s ) )
48 47 eleq1d 
 |-  ( ( f = g /\ a = b ) -> ( ( f |` s ) e. MblFn <-> ( g |` s ) e. MblFn ) )
49 48 ralbidv 
 |-  ( ( f = g /\ a = b ) -> ( A. s e. t ( f |` s ) e. MblFn <-> A. s e. t ( g |` s ) e. MblFn ) )
50 45 49 anbi12d 
 |-  ( ( f = g /\ a = b ) -> ( ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) <-> ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) ) )
51 eqeq2 
 |-  ( a = b -> ( U. t = a <-> U. t = b ) )
52 51 adantl 
 |-  ( ( f = g /\ a = b ) -> ( U. t = a <-> U. t = b ) )
53 50 52 anbi12d 
 |-  ( ( f = g /\ a = b ) -> ( ( ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) /\ U. t = a ) <-> ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) ) )
54 eleq1 
 |-  ( f = g -> ( f e. MblFn <-> g e. MblFn ) )
55 54 adantr 
 |-  ( ( f = g /\ a = b ) -> ( f e. MblFn <-> g e. MblFn ) )
56 53 55 imbi12d 
 |-  ( ( f = g /\ a = b ) -> ( ( ( ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) /\ U. t = a ) -> f e. MblFn ) <-> ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) ) )
57 56 cbval2vw 
 |-  ( A. f A. a ( ( ( f : a --> CC /\ A. s e. t ( f |` s ) e. MblFn ) /\ U. t = a ) -> f e. MblFn ) <-> A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) )
58 42 57 bitrdi 
 |-  ( r = t -> ( A. f A. a ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) ) )
59 raleq 
 |-  ( r = ( t u. { h } ) -> ( A. s e. r ( f |` s ) e. MblFn <-> A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) )
60 59 anbi2d 
 |-  ( r = ( t u. { h } ) -> ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) <-> ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) ) )
61 unieq 
 |-  ( r = ( t u. { h } ) -> U. r = U. ( t u. { h } ) )
62 61 eqeq1d 
 |-  ( r = ( t u. { h } ) -> ( U. r = a <-> U. ( t u. { h } ) = a ) )
63 60 62 anbi12d 
 |-  ( r = ( t u. { h } ) -> ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) <-> ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) )
64 63 imbi1d 
 |-  ( r = ( t u. { h } ) -> ( ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> f e. MblFn ) ) )
65 64 2albidv 
 |-  ( r = ( t u. { h } ) -> ( A. f A. a ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> A. f A. a ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> f e. MblFn ) ) )
66 raleq 
 |-  ( r = S -> ( A. s e. r ( f |` s ) e. MblFn <-> A. s e. S ( f |` s ) e. MblFn ) )
67 66 anbi2d 
 |-  ( r = S -> ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) <-> ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) ) )
68 unieq 
 |-  ( r = S -> U. r = U. S )
69 68 eqeq1d 
 |-  ( r = S -> ( U. r = a <-> U. S = a ) )
70 67 69 anbi12d 
 |-  ( r = S -> ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) <-> ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) ) )
71 70 imbi1d 
 |-  ( r = S -> ( ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) ) )
72 71 2albidv 
 |-  ( r = S -> ( A. f A. a ( ( ( f : a --> CC /\ A. s e. r ( f |` s ) e. MblFn ) /\ U. r = a ) -> f e. MblFn ) <-> A. f A. a ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) ) )
73 frel 
 |-  ( f : a --> CC -> Rel f )
74 73 adantr 
 |-  ( ( f : a --> CC /\ (/) = a ) -> Rel f )
75 fdm 
 |-  ( f : a --> CC -> dom f = a )
76 eqcom 
 |-  ( (/) = a <-> a = (/) )
77 76 biimpi 
 |-  ( (/) = a -> a = (/) )
78 75 77 sylan9eq 
 |-  ( ( f : a --> CC /\ (/) = a ) -> dom f = (/) )
79 reldm0 
 |-  ( Rel f -> ( f = (/) <-> dom f = (/) ) )
80 79 biimpar 
 |-  ( ( Rel f /\ dom f = (/) ) -> f = (/) )
81 mbf0 
 |-  (/) e. MblFn
82 80 81 eqeltrdi 
 |-  ( ( Rel f /\ dom f = (/) ) -> f e. MblFn )
83 74 78 82 syl2anc 
 |-  ( ( f : a --> CC /\ (/) = a ) -> f e. MblFn )
84 83 gen2 
 |-  A. f A. a ( ( f : a --> CC /\ (/) = a ) -> f e. MblFn )
85 ref 
 |-  Re : CC --> RR
86 fco 
 |-  ( ( Re : CC --> RR /\ f : a --> CC ) -> ( Re o. f ) : a --> RR )
87 85 86 mpan 
 |-  ( f : a --> CC -> ( Re o. f ) : a --> RR )
88 87 adantr 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> ( Re o. f ) : a --> RR )
89 88 ad2antrl 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( Re o. f ) : a --> RR )
90 recncf 
 |-  Re e. ( CC -cn-> RR )
91 90 elexi 
 |-  Re e. _V
92 vex 
 |-  f e. _V
93 91 92 coex 
 |-  ( Re o. f ) e. _V
94 93 resex 
 |-  ( ( Re o. f ) |` U. t ) e. _V
95 vuniex 
 |-  U. t e. _V
96 eqcom 
 |-  ( b = U. t <-> U. t = b )
97 96 biimpi 
 |-  ( b = U. t -> U. t = b )
98 97 adantl 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> U. t = b )
99 98 biantrud 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) <-> ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) ) )
100 eqid 
 |-  CC = CC
101 feq123 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t /\ CC = CC ) -> ( g : b --> CC <-> ( ( Re o. f ) |` U. t ) : U. t --> CC ) )
102 100 101 mp3an3 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( g : b --> CC <-> ( ( Re o. f ) |` U. t ) : U. t --> CC ) )
103 reseq1 
 |-  ( g = ( ( Re o. f ) |` U. t ) -> ( g |` s ) = ( ( ( Re o. f ) |` U. t ) |` s ) )
104 103 eleq1d 
 |-  ( g = ( ( Re o. f ) |` U. t ) -> ( ( g |` s ) e. MblFn <-> ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) )
105 104 adantr 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( ( g |` s ) e. MblFn <-> ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) )
106 105 ralbidv 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( A. s e. t ( g |` s ) e. MblFn <-> A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) )
107 102 106 anbi12d 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) <-> ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) ) )
108 99 107 bitr3d 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) <-> ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) ) )
109 eleq1 
 |-  ( g = ( ( Re o. f ) |` U. t ) -> ( g e. MblFn <-> ( ( Re o. f ) |` U. t ) e. MblFn ) )
110 109 adantr 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( g e. MblFn <-> ( ( Re o. f ) |` U. t ) e. MblFn ) )
111 108 110 imbi12d 
 |-  ( ( g = ( ( Re o. f ) |` U. t ) /\ b = U. t ) -> ( ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) <-> ( ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Re o. f ) |` U. t ) e. MblFn ) ) )
112 111 spc2gv 
 |-  ( ( ( ( Re o. f ) |` U. t ) e. _V /\ U. t e. _V ) -> ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) -> ( ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Re o. f ) |` U. t ) e. MblFn ) ) )
113 94 95 112 mp2an 
 |-  ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) -> ( ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Re o. f ) |` U. t ) e. MblFn ) )
114 ax-resscn 
 |-  RR C_ CC
115 fss 
 |-  ( ( Re : CC --> RR /\ RR C_ CC ) -> Re : CC --> CC )
116 85 114 115 mp2an 
 |-  Re : CC --> CC
117 fco 
 |-  ( ( Re : CC --> CC /\ f : a --> CC ) -> ( Re o. f ) : a --> CC )
118 116 117 mpan 
 |-  ( f : a --> CC -> ( Re o. f ) : a --> CC )
119 ssun1 
 |-  t C_ ( t u. { h } )
120 119 unissi 
 |-  U. t C_ U. ( t u. { h } )
121 id 
 |-  ( U. ( t u. { h } ) = a -> U. ( t u. { h } ) = a )
122 120 121 sseqtrid 
 |-  ( U. ( t u. { h } ) = a -> U. t C_ a )
123 fssres 
 |-  ( ( ( Re o. f ) : a --> CC /\ U. t C_ a ) -> ( ( Re o. f ) |` U. t ) : U. t --> CC )
124 118 122 123 syl2an 
 |-  ( ( f : a --> CC /\ U. ( t u. { h } ) = a ) -> ( ( Re o. f ) |` U. t ) : U. t --> CC )
125 124 adantlr 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> ( ( Re o. f ) |` U. t ) : U. t --> CC )
126 elssuni 
 |-  ( r e. t -> r C_ U. t )
127 126 resabs1d 
 |-  ( r e. t -> ( ( ( Re o. f ) |` U. t ) |` r ) = ( ( Re o. f ) |` r ) )
128 resco 
 |-  ( ( Re o. f ) |` r ) = ( Re o. ( f |` r ) )
129 127 128 eqtrdi 
 |-  ( r e. t -> ( ( ( Re o. f ) |` U. t ) |` r ) = ( Re o. ( f |` r ) ) )
130 129 adantl 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( ( ( Re o. f ) |` U. t ) |` r ) = ( Re o. ( f |` r ) ) )
131 elun1 
 |-  ( r e. t -> r e. ( t u. { h } ) )
132 reseq2 
 |-  ( s = r -> ( f |` s ) = ( f |` r ) )
133 132 eleq1d 
 |-  ( s = r -> ( ( f |` s ) e. MblFn <-> ( f |` r ) e. MblFn ) )
134 133 rspccva 
 |-  ( ( A. s e. ( t u. { h } ) ( f |` s ) e. MblFn /\ r e. ( t u. { h } ) ) -> ( f |` r ) e. MblFn )
135 131 134 sylan2 
 |-  ( ( A. s e. ( t u. { h } ) ( f |` s ) e. MblFn /\ r e. t ) -> ( f |` r ) e. MblFn )
136 135 adantll 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( f |` r ) e. MblFn )
137 fresin 
 |-  ( f : a --> CC -> ( f |` r ) : ( a i^i r ) --> CC )
138 ismbfcn 
 |-  ( ( f |` r ) : ( a i^i r ) --> CC -> ( ( f |` r ) e. MblFn <-> ( ( Re o. ( f |` r ) ) e. MblFn /\ ( Im o. ( f |` r ) ) e. MblFn ) ) )
139 137 138 syl 
 |-  ( f : a --> CC -> ( ( f |` r ) e. MblFn <-> ( ( Re o. ( f |` r ) ) e. MblFn /\ ( Im o. ( f |` r ) ) e. MblFn ) ) )
140 139 biimpd 
 |-  ( f : a --> CC -> ( ( f |` r ) e. MblFn -> ( ( Re o. ( f |` r ) ) e. MblFn /\ ( Im o. ( f |` r ) ) e. MblFn ) ) )
141 140 ad2antrr 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( ( f |` r ) e. MblFn -> ( ( Re o. ( f |` r ) ) e. MblFn /\ ( Im o. ( f |` r ) ) e. MblFn ) ) )
142 136 141 mpd 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( ( Re o. ( f |` r ) ) e. MblFn /\ ( Im o. ( f |` r ) ) e. MblFn ) )
143 142 simpld 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( Re o. ( f |` r ) ) e. MblFn )
144 130 143 eqeltrd 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( ( ( Re o. f ) |` U. t ) |` r ) e. MblFn )
145 144 ralrimiva 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> A. r e. t ( ( ( Re o. f ) |` U. t ) |` r ) e. MblFn )
146 reseq2 
 |-  ( r = s -> ( ( ( Re o. f ) |` U. t ) |` r ) = ( ( ( Re o. f ) |` U. t ) |` s ) )
147 146 eleq1d 
 |-  ( r = s -> ( ( ( ( Re o. f ) |` U. t ) |` r ) e. MblFn <-> ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) )
148 147 cbvralvw 
 |-  ( A. r e. t ( ( ( Re o. f ) |` U. t ) |` r ) e. MblFn <-> A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn )
149 145 148 sylib 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn )
150 149 adantr 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn )
151 pm2.27 
 |-  ( ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Re o. f ) |` U. t ) e. MblFn ) -> ( ( Re o. f ) |` U. t ) e. MblFn ) )
152 125 150 151 syl2anc 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> ( ( ( ( ( Re o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Re o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Re o. f ) |` U. t ) e. MblFn ) -> ( ( Re o. f ) |` U. t ) e. MblFn ) )
153 113 152 mpan9 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( ( Re o. f ) |` U. t ) e. MblFn )
154 vsnid 
 |-  h e. { h }
155 elun2 
 |-  ( h e. { h } -> h e. ( t u. { h } ) )
156 reseq2 
 |-  ( s = h -> ( f |` s ) = ( f |` h ) )
157 156 eleq1d 
 |-  ( s = h -> ( ( f |` s ) e. MblFn <-> ( f |` h ) e. MblFn ) )
158 157 rspcv 
 |-  ( h e. ( t u. { h } ) -> ( A. s e. ( t u. { h } ) ( f |` s ) e. MblFn -> ( f |` h ) e. MblFn ) )
159 154 155 158 mp2b 
 |-  ( A. s e. ( t u. { h } ) ( f |` s ) e. MblFn -> ( f |` h ) e. MblFn )
160 resco 
 |-  ( ( Re o. f ) |` h ) = ( Re o. ( f |` h ) )
161 fresin 
 |-  ( f : a --> CC -> ( f |` h ) : ( a i^i h ) --> CC )
162 ismbfcn 
 |-  ( ( f |` h ) : ( a i^i h ) --> CC -> ( ( f |` h ) e. MblFn <-> ( ( Re o. ( f |` h ) ) e. MblFn /\ ( Im o. ( f |` h ) ) e. MblFn ) ) )
163 161 162 syl 
 |-  ( f : a --> CC -> ( ( f |` h ) e. MblFn <-> ( ( Re o. ( f |` h ) ) e. MblFn /\ ( Im o. ( f |` h ) ) e. MblFn ) ) )
164 163 simprbda 
 |-  ( ( f : a --> CC /\ ( f |` h ) e. MblFn ) -> ( Re o. ( f |` h ) ) e. MblFn )
165 160 164 eqeltrid 
 |-  ( ( f : a --> CC /\ ( f |` h ) e. MblFn ) -> ( ( Re o. f ) |` h ) e. MblFn )
166 159 165 sylan2 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> ( ( Re o. f ) |` h ) e. MblFn )
167 166 ad2antrl 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( ( Re o. f ) |` h ) e. MblFn )
168 uniun 
 |-  U. ( t u. { h } ) = ( U. t u. U. { h } )
169 vex 
 |-  h e. _V
170 169 unisn 
 |-  U. { h } = h
171 170 uneq2i 
 |-  ( U. t u. U. { h } ) = ( U. t u. h )
172 168 171 eqtri 
 |-  U. ( t u. { h } ) = ( U. t u. h )
173 172 121 syl5eqr 
 |-  ( U. ( t u. { h } ) = a -> ( U. t u. h ) = a )
174 173 ad2antll 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( U. t u. h ) = a )
175 89 153 167 174 mbfres2 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( Re o. f ) e. MblFn )
176 imf 
 |-  Im : CC --> RR
177 fco 
 |-  ( ( Im : CC --> RR /\ f : a --> CC ) -> ( Im o. f ) : a --> RR )
178 176 177 mpan 
 |-  ( f : a --> CC -> ( Im o. f ) : a --> RR )
179 178 adantr 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> ( Im o. f ) : a --> RR )
180 179 ad2antrl 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( Im o. f ) : a --> RR )
181 imcncf 
 |-  Im e. ( CC -cn-> RR )
182 181 elexi 
 |-  Im e. _V
183 182 92 coex 
 |-  ( Im o. f ) e. _V
184 183 resex 
 |-  ( ( Im o. f ) |` U. t ) e. _V
185 97 adantl 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> U. t = b )
186 185 biantrud 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) <-> ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) ) )
187 feq123 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t /\ CC = CC ) -> ( g : b --> CC <-> ( ( Im o. f ) |` U. t ) : U. t --> CC ) )
188 100 187 mp3an3 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( g : b --> CC <-> ( ( Im o. f ) |` U. t ) : U. t --> CC ) )
189 reseq1 
 |-  ( g = ( ( Im o. f ) |` U. t ) -> ( g |` s ) = ( ( ( Im o. f ) |` U. t ) |` s ) )
190 189 eleq1d 
 |-  ( g = ( ( Im o. f ) |` U. t ) -> ( ( g |` s ) e. MblFn <-> ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) )
191 190 adantr 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( ( g |` s ) e. MblFn <-> ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) )
192 191 ralbidv 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( A. s e. t ( g |` s ) e. MblFn <-> A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) )
193 188 192 anbi12d 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) <-> ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) ) )
194 186 193 bitr3d 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) <-> ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) ) )
195 eleq1 
 |-  ( g = ( ( Im o. f ) |` U. t ) -> ( g e. MblFn <-> ( ( Im o. f ) |` U. t ) e. MblFn ) )
196 195 adantr 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( g e. MblFn <-> ( ( Im o. f ) |` U. t ) e. MblFn ) )
197 194 196 imbi12d 
 |-  ( ( g = ( ( Im o. f ) |` U. t ) /\ b = U. t ) -> ( ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) <-> ( ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Im o. f ) |` U. t ) e. MblFn ) ) )
198 197 spc2gv 
 |-  ( ( ( ( Im o. f ) |` U. t ) e. _V /\ U. t e. _V ) -> ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) -> ( ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Im o. f ) |` U. t ) e. MblFn ) ) )
199 184 95 198 mp2an 
 |-  ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) -> ( ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Im o. f ) |` U. t ) e. MblFn ) )
200 fss 
 |-  ( ( Im : CC --> RR /\ RR C_ CC ) -> Im : CC --> CC )
201 176 114 200 mp2an 
 |-  Im : CC --> CC
202 fco 
 |-  ( ( Im : CC --> CC /\ f : a --> CC ) -> ( Im o. f ) : a --> CC )
203 201 202 mpan 
 |-  ( f : a --> CC -> ( Im o. f ) : a --> CC )
204 fssres 
 |-  ( ( ( Im o. f ) : a --> CC /\ U. t C_ a ) -> ( ( Im o. f ) |` U. t ) : U. t --> CC )
205 203 122 204 syl2an 
 |-  ( ( f : a --> CC /\ U. ( t u. { h } ) = a ) -> ( ( Im o. f ) |` U. t ) : U. t --> CC )
206 205 adantlr 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> ( ( Im o. f ) |` U. t ) : U. t --> CC )
207 126 resabs1d 
 |-  ( r e. t -> ( ( ( Im o. f ) |` U. t ) |` r ) = ( ( Im o. f ) |` r ) )
208 resco 
 |-  ( ( Im o. f ) |` r ) = ( Im o. ( f |` r ) )
209 207 208 eqtrdi 
 |-  ( r e. t -> ( ( ( Im o. f ) |` U. t ) |` r ) = ( Im o. ( f |` r ) ) )
210 209 adantl 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( ( ( Im o. f ) |` U. t ) |` r ) = ( Im o. ( f |` r ) ) )
211 142 simprd 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( Im o. ( f |` r ) ) e. MblFn )
212 210 211 eqeltrd 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ r e. t ) -> ( ( ( Im o. f ) |` U. t ) |` r ) e. MblFn )
213 212 ralrimiva 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> A. r e. t ( ( ( Im o. f ) |` U. t ) |` r ) e. MblFn )
214 reseq2 
 |-  ( r = s -> ( ( ( Im o. f ) |` U. t ) |` r ) = ( ( ( Im o. f ) |` U. t ) |` s ) )
215 214 eleq1d 
 |-  ( r = s -> ( ( ( ( Im o. f ) |` U. t ) |` r ) e. MblFn <-> ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) )
216 215 cbvralvw 
 |-  ( A. r e. t ( ( ( Im o. f ) |` U. t ) |` r ) e. MblFn <-> A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn )
217 213 216 sylib 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn )
218 217 adantr 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn )
219 pm2.27 
 |-  ( ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Im o. f ) |` U. t ) e. MblFn ) -> ( ( Im o. f ) |` U. t ) e. MblFn ) )
220 206 218 219 syl2anc 
 |-  ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> ( ( ( ( ( Im o. f ) |` U. t ) : U. t --> CC /\ A. s e. t ( ( ( Im o. f ) |` U. t ) |` s ) e. MblFn ) -> ( ( Im o. f ) |` U. t ) e. MblFn ) -> ( ( Im o. f ) |` U. t ) e. MblFn ) )
221 199 220 mpan9 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( ( Im o. f ) |` U. t ) e. MblFn )
222 resco 
 |-  ( ( Im o. f ) |` h ) = ( Im o. ( f |` h ) )
223 163 simplbda 
 |-  ( ( f : a --> CC /\ ( f |` h ) e. MblFn ) -> ( Im o. ( f |` h ) ) e. MblFn )
224 222 223 eqeltrid 
 |-  ( ( f : a --> CC /\ ( f |` h ) e. MblFn ) -> ( ( Im o. f ) |` h ) e. MblFn )
225 159 224 sylan2 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> ( ( Im o. f ) |` h ) e. MblFn )
226 225 ad2antrl 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( ( Im o. f ) |` h ) e. MblFn )
227 180 221 226 174 mbfres2 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( Im o. f ) e. MblFn )
228 ismbfcn 
 |-  ( f : a --> CC -> ( f e. MblFn <-> ( ( Re o. f ) e. MblFn /\ ( Im o. f ) e. MblFn ) ) )
229 228 adantr 
 |-  ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) -> ( f e. MblFn <-> ( ( Re o. f ) e. MblFn /\ ( Im o. f ) e. MblFn ) ) )
230 229 ad2antrl 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> ( f e. MblFn <-> ( ( Re o. f ) e. MblFn /\ ( Im o. f ) e. MblFn ) ) )
231 175 227 230 mpbir2and 
 |-  ( ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) /\ ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) ) -> f e. MblFn )
232 231 ex 
 |-  ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) -> ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> f e. MblFn ) )
233 232 alrimivv 
 |-  ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) -> A. f A. a ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> f e. MblFn ) )
234 233 a1i 
 |-  ( t e. Fin -> ( A. g A. b ( ( ( g : b --> CC /\ A. s e. t ( g |` s ) e. MblFn ) /\ U. t = b ) -> g e. MblFn ) -> A. f A. a ( ( ( f : a --> CC /\ A. s e. ( t u. { h } ) ( f |` s ) e. MblFn ) /\ U. ( t u. { h } ) = a ) -> f e. MblFn ) ) )
235 35 58 65 72 84 234 findcard2 
 |-  ( S e. Fin -> A. f A. a ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) )
236 2sp 
 |-  ( A. f A. a ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) -> ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) )
237 2 235 236 3syl 
 |-  ( ph -> ( ( ( f : a --> CC /\ A. s e. S ( f |` s ) e. MblFn ) /\ U. S = a ) -> f e. MblFn ) )
238 16 25 237 vtocl2g 
 |-  ( ( A e. _V /\ F e. _V ) -> ( ph -> ( ( ( F : A --> CC /\ A. s e. S ( F |` s ) e. MblFn ) /\ U. S = A ) -> F e. MblFn ) ) )
239 10 238 mpcom 
 |-  ( ph -> ( ( ( F : A --> CC /\ A. s e. S ( F |` s ) e. MblFn ) /\ U. S = A ) -> F e. MblFn ) )
240 4 239 mpan2d 
 |-  ( ph -> ( ( F : A --> CC /\ A. s e. S ( F |` s ) e. MblFn ) -> F e. MblFn ) )
241 1 3 240 mp2and 
 |-  ( ph -> F e. MblFn )