Metamath Proof Explorer

Theorem mbfimaopnlem

Description: Lemma for mbfimaopn . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses mbfimaopn.1 
|- J = ( TopOpen ` CCfld )
mbfimaopn.2 
|- G = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
mbfimaopn.3 
|- B = ( (,) " ( QQ X. QQ ) )
mbfimaopn.4 
|- K = ran ( x e. B , y e. B |-> ( x X. y ) )
Assertion mbfimaopnlem 
|- ( ( F e. MblFn /\ A e. J ) -> ( `' F " A ) e. dom vol )

Proof

Step Hyp Ref Expression
1 mbfimaopn.1 
 |-  J = ( TopOpen ` CCfld )
2 mbfimaopn.2 
 |-  G = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
3 mbfimaopn.3 
 |-  B = ( (,) " ( QQ X. QQ ) )
4 mbfimaopn.4 
 |-  K = ran ( x e. B , y e. B |-> ( x X. y ) )
5 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
6 2 5 1 cnrehmeo 
 |-  G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Homeo J )
7 hmeocn 
 |-  ( G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Homeo J ) -> G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) )
8 6 7 ax-mp 
 |-  G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J )
9 cnima 
 |-  ( ( G e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) /\ A e. J ) -> ( `' G " A ) e. ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) )
10 8 9 mpan 
 |-  ( A e. J -> ( `' G " A ) e. ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) )
11 3 fveq2i 
 |-  ( topGen ` B ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
12 11 tgqioo 
 |-  ( topGen ` ran (,) ) = ( topGen ` B )
13 12 12 oveq12i 
 |-  ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) = ( ( topGen ` B ) tX ( topGen ` B ) )
14 qtopbas 
 |-  ( (,) " ( QQ X. QQ ) ) e. TopBases
15 3 14 eqeltri 
 |-  B e. TopBases
16 txbasval 
 |-  ( ( B e. TopBases /\ B e. TopBases ) -> ( ( topGen ` B ) tX ( topGen ` B ) ) = ( B tX B ) )
17 15 15 16 mp2an 
 |-  ( ( topGen ` B ) tX ( topGen ` B ) ) = ( B tX B )
18 4 txval 
 |-  ( ( B e. TopBases /\ B e. TopBases ) -> ( B tX B ) = ( topGen ` K ) )
19 15 15 18 mp2an 
 |-  ( B tX B ) = ( topGen ` K )
20 13 17 19 3eqtri 
 |-  ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) = ( topGen ` K )
21 10 20 eleqtrdi 
 |-  ( A e. J -> ( `' G " A ) e. ( topGen ` K ) )
22 4 txbas 
 |-  ( ( B e. TopBases /\ B e. TopBases ) -> K e. TopBases )
23 15 15 22 mp2an 
 |-  K e. TopBases
24 eltg3 
 |-  ( K e. TopBases -> ( ( `' G " A ) e. ( topGen ` K ) <-> E. t ( t C_ K /\ ( `' G " A ) = U. t ) ) )
25 23 24 ax-mp 
 |-  ( ( `' G " A ) e. ( topGen ` K ) <-> E. t ( t C_ K /\ ( `' G " A ) = U. t ) )
26 21 25 sylib 
 |-  ( A e. J -> E. t ( t C_ K /\ ( `' G " A ) = U. t ) )
27 26 adantl 
 |-  ( ( F e. MblFn /\ A e. J ) -> E. t ( t C_ K /\ ( `' G " A ) = U. t ) )
28 2 cnref1o 
 |-  G : ( RR X. RR ) -1-1-onto-> CC
29 f1ofo 
 |-  ( G : ( RR X. RR ) -1-1-onto-> CC -> G : ( RR X. RR ) -onto-> CC )
30 28 29 ax-mp 
 |-  G : ( RR X. RR ) -onto-> CC
31 elssuni 
 |-  ( A e. J -> A C_ U. J )
32 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
33 32 toponunii 
 |-  CC = U. J
34 31 33 sseqtrrdi 
 |-  ( A e. J -> A C_ CC )
35 34 ad2antlr 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> A C_ CC )
36 foimacnv 
 |-  ( ( G : ( RR X. RR ) -onto-> CC /\ A C_ CC ) -> ( G " ( `' G " A ) ) = A )
37 30 35 36 sylancr 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( G " ( `' G " A ) ) = A )
38 simprr 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' G " A ) = U. t )
39 38 imaeq2d 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( G " ( `' G " A ) ) = ( G " U. t ) )
40 imauni 
 |-  ( G " U. t ) = U_ w e. t ( G " w )
41 39 40 eqtrdi 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( G " ( `' G " A ) ) = U_ w e. t ( G " w ) )
42 37 41 eqtr3d 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> A = U_ w e. t ( G " w ) )
43 42 imaeq2d 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' F " A ) = ( `' F " U_ w e. t ( G " w ) ) )
44 imaiun 
 |-  ( `' F " U_ w e. t ( G " w ) ) = U_ w e. t ( `' F " ( G " w ) )
45 43 44 eqtrdi 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' F " A ) = U_ w e. t ( `' F " ( G " w ) ) )
46 ssdomg 
 |-  ( K e. TopBases -> ( t C_ K -> t ~<_ K ) )
47 23 46 ax-mp 
 |-  ( t C_ K -> t ~<_ K )
48 omelon 
 |-  _om e. On
49 nnenom 
 |-  NN ~~ _om
50 49 ensymi 
 |-  _om ~~ NN
51 isnumi 
 |-  ( ( _om e. On /\ _om ~~ NN ) -> NN e. dom card )
52 48 50 51 mp2an 
 |-  NN e. dom card
53 qnnen 
 |-  QQ ~~ NN
54 xpen 
 |-  ( ( QQ ~~ NN /\ QQ ~~ NN ) -> ( QQ X. QQ ) ~~ ( NN X. NN ) )
55 53 53 54 mp2an 
 |-  ( QQ X. QQ ) ~~ ( NN X. NN )
56 xpnnen 
 |-  ( NN X. NN ) ~~ NN
57 55 56 entri 
 |-  ( QQ X. QQ ) ~~ NN
58 57 49 entr2i 
 |-  _om ~~ ( QQ X. QQ )
59 isnumi 
 |-  ( ( _om e. On /\ _om ~~ ( QQ X. QQ ) ) -> ( QQ X. QQ ) e. dom card )
60 48 58 59 mp2an 
 |-  ( QQ X. QQ ) e. dom card
61 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
62 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
63 61 62 ax-mp 
 |-  Fun (,)
64 qssre 
 |-  QQ C_ RR
65 ressxr 
 |-  RR C_ RR*
66 64 65 sstri 
 |-  QQ C_ RR*
67 xpss12 
 |-  ( ( QQ C_ RR* /\ QQ C_ RR* ) -> ( QQ X. QQ ) C_ ( RR* X. RR* ) )
68 66 66 67 mp2an 
 |-  ( QQ X. QQ ) C_ ( RR* X. RR* )
69 61 fdmi 
 |-  dom (,) = ( RR* X. RR* )
70 68 69 sseqtrri 
 |-  ( QQ X. QQ ) C_ dom (,)
71 fores 
 |-  ( ( Fun (,) /\ ( QQ X. QQ ) C_ dom (,) ) -> ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) )
72 63 70 71 mp2an 
 |-  ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) )
73 fodomnum 
 |-  ( ( QQ X. QQ ) e. dom card -> ( ( (,) |` ( QQ X. QQ ) ) : ( QQ X. QQ ) -onto-> ( (,) " ( QQ X. QQ ) ) -> ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ ) ) )
74 60 72 73 mp2 
 |-  ( (,) " ( QQ X. QQ ) ) ~<_ ( QQ X. QQ )
75 3 74 eqbrtri 
 |-  B ~<_ ( QQ X. QQ )
76 domentr 
 |-  ( ( B ~<_ ( QQ X. QQ ) /\ ( QQ X. QQ ) ~~ NN ) -> B ~<_ NN )
77 75 57 76 mp2an 
 |-  B ~<_ NN
78 15 elexi 
 |-  B e. _V
79 78 xpdom1 
 |-  ( B ~<_ NN -> ( B X. B ) ~<_ ( NN X. B ) )
80 77 79 ax-mp 
 |-  ( B X. B ) ~<_ ( NN X. B )
81 nnex 
 |-  NN e. _V
82 81 xpdom2 
 |-  ( B ~<_ NN -> ( NN X. B ) ~<_ ( NN X. NN ) )
83 77 82 ax-mp 
 |-  ( NN X. B ) ~<_ ( NN X. NN )
84 domtr 
 |-  ( ( ( B X. B ) ~<_ ( NN X. B ) /\ ( NN X. B ) ~<_ ( NN X. NN ) ) -> ( B X. B ) ~<_ ( NN X. NN ) )
85 80 83 84 mp2an 
 |-  ( B X. B ) ~<_ ( NN X. NN )
86 domentr 
 |-  ( ( ( B X. B ) ~<_ ( NN X. NN ) /\ ( NN X. NN ) ~~ NN ) -> ( B X. B ) ~<_ NN )
87 85 56 86 mp2an 
 |-  ( B X. B ) ~<_ NN
88 numdom 
 |-  ( ( NN e. dom card /\ ( B X. B ) ~<_ NN ) -> ( B X. B ) e. dom card )
89 52 87 88 mp2an 
 |-  ( B X. B ) e. dom card
90 eqid 
 |-  ( x e. B , y e. B |-> ( x X. y ) ) = ( x e. B , y e. B |-> ( x X. y ) )
91 vex 
 |-  x e. _V
92 vex 
 |-  y e. _V
93 91 92 xpex 
 |-  ( x X. y ) e. _V
94 90 93 fnmpoi 
 |-  ( x e. B , y e. B |-> ( x X. y ) ) Fn ( B X. B )
95 dffn4 
 |-  ( ( x e. B , y e. B |-> ( x X. y ) ) Fn ( B X. B ) <-> ( x e. B , y e. B |-> ( x X. y ) ) : ( B X. B ) -onto-> ran ( x e. B , y e. B |-> ( x X. y ) ) )
96 94 95 mpbi 
 |-  ( x e. B , y e. B |-> ( x X. y ) ) : ( B X. B ) -onto-> ran ( x e. B , y e. B |-> ( x X. y ) )
97 fodomnum 
 |-  ( ( B X. B ) e. dom card -> ( ( x e. B , y e. B |-> ( x X. y ) ) : ( B X. B ) -onto-> ran ( x e. B , y e. B |-> ( x X. y ) ) -> ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ ( B X. B ) ) )
98 89 96 97 mp2 
 |-  ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ ( B X. B )
99 domtr 
 |-  ( ( ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ ( B X. B ) /\ ( B X. B ) ~<_ NN ) -> ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ NN )
100 98 87 99 mp2an 
 |-  ran ( x e. B , y e. B |-> ( x X. y ) ) ~<_ NN
101 4 100 eqbrtri 
 |-  K ~<_ NN
102 domtr 
 |-  ( ( t ~<_ K /\ K ~<_ NN ) -> t ~<_ NN )
103 47 101 102 sylancl 
 |-  ( t C_ K -> t ~<_ NN )
104 103 ad2antrl 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> t ~<_ NN )
105 4 eleq2i 
 |-  ( w e. K <-> w e. ran ( x e. B , y e. B |-> ( x X. y ) ) )
106 90 93 elrnmpo 
 |-  ( w e. ran ( x e. B , y e. B |-> ( x X. y ) ) <-> E. x e. B E. y e. B w = ( x X. y ) )
107 105 106 bitri 
 |-  ( w e. K <-> E. x e. B E. y e. B w = ( x X. y ) )
108 elin 
 |-  ( z e. ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) <-> ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) )
109 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
110 109 adantr 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> F : dom F --> CC )
111 fvco3 
 |-  ( ( F : dom F --> CC /\ z e. dom F ) -> ( ( Re o. F ) ` z ) = ( Re ` ( F ` z ) ) )
112 110 111 sylan 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( Re o. F ) ` z ) = ( Re ` ( F ` z ) ) )
113 112 eleq1d 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( Re o. F ) ` z ) e. x <-> ( Re ` ( F ` z ) ) e. x ) )
114 fvco3 
 |-  ( ( F : dom F --> CC /\ z e. dom F ) -> ( ( Im o. F ) ` z ) = ( Im ` ( F ` z ) ) )
115 110 114 sylan 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( Im o. F ) ` z ) = ( Im ` ( F ` z ) ) )
116 115 eleq1d 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( Im o. F ) ` z ) e. y <-> ( Im ` ( F ` z ) ) e. y ) )
117 113 116 anbi12d 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) <-> ( ( Re ` ( F ` z ) ) e. x /\ ( Im ` ( F ` z ) ) e. y ) ) )
118 110 ffvelcdmda 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( F ` z ) e. CC )
119 fveq2 
 |-  ( w = ( F ` z ) -> ( Re ` w ) = ( Re ` ( F ` z ) ) )
120 fveq2 
 |-  ( w = ( F ` z ) -> ( Im ` w ) = ( Im ` ( F ` z ) ) )
121 119 120 opeq12d 
 |-  ( w = ( F ` z ) -> <. ( Re ` w ) , ( Im ` w ) >. = <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. )
122 2 cnrecnv 
 |-  `' G = ( w e. CC |-> <. ( Re ` w ) , ( Im ` w ) >. )
123 opex 
 |-  <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. _V
124 121 122 123 fvmpt 
 |-  ( ( F ` z ) e. CC -> ( `' G ` ( F ` z ) ) = <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. )
125 118 124 syl 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( `' G ` ( F ` z ) ) = <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. )
126 125 eleq1d 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( `' G ` ( F ` z ) ) e. ( x X. y ) <-> <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. ( x X. y ) ) )
127 118 biantrurd 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( `' G ` ( F ` z ) ) e. ( x X. y ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) ) )
128 126 127 bitr3d 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. ( x X. y ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) ) )
129 opelxp 
 |-  ( <. ( Re ` ( F ` z ) ) , ( Im ` ( F ` z ) ) >. e. ( x X. y ) <-> ( ( Re ` ( F ` z ) ) e. x /\ ( Im ` ( F ` z ) ) e. y ) )
130 f1ocnv 
 |-  ( G : ( RR X. RR ) -1-1-onto-> CC -> `' G : CC -1-1-onto-> ( RR X. RR ) )
131 f1ofn 
 |-  ( `' G : CC -1-1-onto-> ( RR X. RR ) -> `' G Fn CC )
132 28 130 131 mp2b 
 |-  `' G Fn CC
133 elpreima 
 |-  ( `' G Fn CC -> ( ( F ` z ) e. ( `' `' G " ( x X. y ) ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) ) )
134 132 133 ax-mp 
 |-  ( ( F ` z ) e. ( `' `' G " ( x X. y ) ) <-> ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) )
135 imacnvcnv 
 |-  ( `' `' G " ( x X. y ) ) = ( G " ( x X. y ) )
136 135 eleq2i 
 |-  ( ( F ` z ) e. ( `' `' G " ( x X. y ) ) <-> ( F ` z ) e. ( G " ( x X. y ) ) )
137 134 136 bitr3i 
 |-  ( ( ( F ` z ) e. CC /\ ( `' G ` ( F ` z ) ) e. ( x X. y ) ) <-> ( F ` z ) e. ( G " ( x X. y ) ) )
138 128 129 137 3bitr3g 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( Re ` ( F ` z ) ) e. x /\ ( Im ` ( F ` z ) ) e. y ) <-> ( F ` z ) e. ( G " ( x X. y ) ) ) )
139 117 138 bitrd 
 |-  ( ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) /\ z e. dom F ) -> ( ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) <-> ( F ` z ) e. ( G " ( x X. y ) ) ) )
140 139 pm5.32da 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) )
141 ref 
 |-  Re : CC --> RR
142 fco 
 |-  ( ( Re : CC --> RR /\ F : dom F --> CC ) -> ( Re o. F ) : dom F --> RR )
143 141 109 142 sylancr 
 |-  ( F e. MblFn -> ( Re o. F ) : dom F --> RR )
144 ffn 
 |-  ( ( Re o. F ) : dom F --> RR -> ( Re o. F ) Fn dom F )
145 elpreima 
 |-  ( ( Re o. F ) Fn dom F -> ( z e. ( `' ( Re o. F ) " x ) <-> ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) ) )
146 143 144 145 3syl 
 |-  ( F e. MblFn -> ( z e. ( `' ( Re o. F ) " x ) <-> ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) ) )
147 imf 
 |-  Im : CC --> RR
148 fco 
 |-  ( ( Im : CC --> RR /\ F : dom F --> CC ) -> ( Im o. F ) : dom F --> RR )
149 147 109 148 sylancr 
 |-  ( F e. MblFn -> ( Im o. F ) : dom F --> RR )
150 ffn 
 |-  ( ( Im o. F ) : dom F --> RR -> ( Im o. F ) Fn dom F )
151 elpreima 
 |-  ( ( Im o. F ) Fn dom F -> ( z e. ( `' ( Im o. F ) " y ) <-> ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) )
152 149 150 151 3syl 
 |-  ( F e. MblFn -> ( z e. ( `' ( Im o. F ) " y ) <-> ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) )
153 146 152 anbi12d 
 |-  ( F e. MblFn -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> ( ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) /\ ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) ) )
154 anandi 
 |-  ( ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) <-> ( ( z e. dom F /\ ( ( Re o. F ) ` z ) e. x ) /\ ( z e. dom F /\ ( ( Im o. F ) ` z ) e. y ) ) )
155 153 154 bitr4di 
 |-  ( F e. MblFn -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) ) )
156 155 adantr 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> ( z e. dom F /\ ( ( ( Re o. F ) ` z ) e. x /\ ( ( Im o. F ) ` z ) e. y ) ) ) )
157 ffn 
 |-  ( F : dom F --> CC -> F Fn dom F )
158 elpreima 
 |-  ( F Fn dom F -> ( z e. ( `' F " ( G " ( x X. y ) ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) )
159 109 157 158 3syl 
 |-  ( F e. MblFn -> ( z e. ( `' F " ( G " ( x X. y ) ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) )
160 159 adantr 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( z e. ( `' F " ( G " ( x X. y ) ) ) <-> ( z e. dom F /\ ( F ` z ) e. ( G " ( x X. y ) ) ) ) )
161 140 156 160 3bitr4d 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( z e. ( `' ( Re o. F ) " x ) /\ z e. ( `' ( Im o. F ) " y ) ) <-> z e. ( `' F " ( G " ( x X. y ) ) ) ) )
162 108 161 bitrid 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( z e. ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) <-> z e. ( `' F " ( G " ( x X. y ) ) ) ) )
163 162 eqrdv 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) = ( `' F " ( G " ( x X. y ) ) ) )
164 ismbfcn 
 |-  ( F : dom F --> CC -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
165 109 164 syl 
 |-  ( F e. MblFn -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
166 165 ibi 
 |-  ( F e. MblFn -> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) )
167 166 simpld 
 |-  ( F e. MblFn -> ( Re o. F ) e. MblFn )
168 ismbf 
 |-  ( ( Re o. F ) : dom F --> RR -> ( ( Re o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) )
169 143 168 syl 
 |-  ( F e. MblFn -> ( ( Re o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) )
170 167 169 mpbid 
 |-  ( F e. MblFn -> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol )
171 170 adantr 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol )
172 imassrn 
 |-  ( (,) " ( QQ X. QQ ) ) C_ ran (,)
173 3 172 eqsstri 
 |-  B C_ ran (,)
174 simprl 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> x e. B )
175 173 174 sselid 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> x e. ran (,) )
176 rsp 
 |-  ( A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol -> ( x e. ran (,) -> ( `' ( Re o. F ) " x ) e. dom vol ) )
177 171 175 176 sylc 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( `' ( Re o. F ) " x ) e. dom vol )
178 166 simprd 
 |-  ( F e. MblFn -> ( Im o. F ) e. MblFn )
179 ismbf 
 |-  ( ( Im o. F ) : dom F --> RR -> ( ( Im o. F ) e. MblFn <-> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol ) )
180 149 179 syl 
 |-  ( F e. MblFn -> ( ( Im o. F ) e. MblFn <-> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol ) )
181 178 180 mpbid 
 |-  ( F e. MblFn -> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol )
182 181 adantr 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol )
183 simprr 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> y e. B )
184 173 183 sselid 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> y e. ran (,) )
185 rsp 
 |-  ( A. y e. ran (,) ( `' ( Im o. F ) " y ) e. dom vol -> ( y e. ran (,) -> ( `' ( Im o. F ) " y ) e. dom vol ) )
186 182 184 185 sylc 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( `' ( Im o. F ) " y ) e. dom vol )
187 inmbl 
 |-  ( ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " y ) e. dom vol ) -> ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) e. dom vol )
188 177 186 187 syl2anc 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( ( `' ( Re o. F ) " x ) i^i ( `' ( Im o. F ) " y ) ) e. dom vol )
189 163 188 eqeltrrd 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( `' F " ( G " ( x X. y ) ) ) e. dom vol )
190 imaeq2 
 |-  ( w = ( x X. y ) -> ( G " w ) = ( G " ( x X. y ) ) )
191 190 imaeq2d 
 |-  ( w = ( x X. y ) -> ( `' F " ( G " w ) ) = ( `' F " ( G " ( x X. y ) ) ) )
192 191 eleq1d 
 |-  ( w = ( x X. y ) -> ( ( `' F " ( G " w ) ) e. dom vol <-> ( `' F " ( G " ( x X. y ) ) ) e. dom vol ) )
193 189 192 syl5ibrcom 
 |-  ( ( F e. MblFn /\ ( x e. B /\ y e. B ) ) -> ( w = ( x X. y ) -> ( `' F " ( G " w ) ) e. dom vol ) )
194 193 rexlimdvva 
 |-  ( F e. MblFn -> ( E. x e. B E. y e. B w = ( x X. y ) -> ( `' F " ( G " w ) ) e. dom vol ) )
195 107 194 biimtrid 
 |-  ( F e. MblFn -> ( w e. K -> ( `' F " ( G " w ) ) e. dom vol ) )
196 195 ralrimiv 
 |-  ( F e. MblFn -> A. w e. K ( `' F " ( G " w ) ) e. dom vol )
197 ssralv 
 |-  ( t C_ K -> ( A. w e. K ( `' F " ( G " w ) ) e. dom vol -> A. w e. t ( `' F " ( G " w ) ) e. dom vol ) )
198 196 197 mpan9 
 |-  ( ( F e. MblFn /\ t C_ K ) -> A. w e. t ( `' F " ( G " w ) ) e. dom vol )
199 198 ad2ant2r 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> A. w e. t ( `' F " ( G " w ) ) e. dom vol )
200 iunmbl2 
 |-  ( ( t ~<_ NN /\ A. w e. t ( `' F " ( G " w ) ) e. dom vol ) -> U_ w e. t ( `' F " ( G " w ) ) e. dom vol )
201 104 199 200 syl2anc 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> U_ w e. t ( `' F " ( G " w ) ) e. dom vol )
202 45 201 eqeltrd 
 |-  ( ( ( F e. MblFn /\ A e. J ) /\ ( t C_ K /\ ( `' G " A ) = U. t ) ) -> ( `' F " A ) e. dom vol )
203 27 202 exlimddv 
 |-  ( ( F e. MblFn /\ A e. J ) -> ( `' F " A ) e. dom vol )