MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfimaopnlem Structured version   Unicode version

Theorem mbfimaopnlem 21145
Description: Lemma for mbfimaopn 21146. (Contributed by Mario Carneiro, 25-Aug-2014.)
Hypotheses
Ref Expression
mbfimaopn.1  |-  J  =  ( TopOpen ` fld )
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
Ref Expression
mbfimaopnlem  |-  ( ( F  e. MblFn  /\  A  e.  J )  ->  ( `' F " A )  e.  dom  vol )
Distinct variable groups:    x, A    x, y, B    x, F, y    x, G, y    x, J, y
Allowed substitution hints:    A( y)    K( x, y)

Proof of Theorem mbfimaopnlem
Dummy variables  t 
z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbfimaopn.2 . . . . . . . 8  |-  G  =  ( x  e.  RR ,  y  e.  RR  |->  ( x  +  (
_i  x.  y )
) )
2 eqid 2443 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
3 mbfimaopn.1 . . . . . . . 8  |-  J  =  ( TopOpen ` fld )
41, 2, 3cnrehmeo 20537 . . . . . . 7  |-  G  e.  ( ( ( topGen ` 
ran  (,) )  tX  ( topGen `
 ran  (,) )
) Homeo J )
5 hmeocn 19345 . . . . . . 7  |-  ( G  e.  ( ( (
topGen `  ran  (,) )  tX  ( topGen `  ran  (,) )
) Homeo J )  ->  G  e.  ( (
( topGen `  ran  (,) )  tX  ( topGen `  ran  (,) )
)  Cn  J ) )
64, 5ax-mp 5 . . . . . 6  |-  G  e.  ( ( ( topGen ` 
ran  (,) )  tX  ( topGen `
 ran  (,) )
)  Cn  J )
7 cnima 18881 . . . . . 6  |-  ( ( G  e.  ( ( ( topGen `  ran  (,) )  tX  ( topGen `  ran  (,) )
)  Cn  J )  /\  A  e.  J
)  ->  ( `' G " A )  e.  ( ( topGen `  ran  (,) )  tX  ( topGen ` 
ran  (,) ) ) )
86, 7mpan 670 . . . . 5  |-  ( A  e.  J  ->  ( `' G " A )  e.  ( ( topGen ` 
ran  (,) )  tX  ( topGen `
 ran  (,) )
) )
9 mbfimaopn.3 . . . . . . . . 9  |-  B  =  ( (,) " ( QQ  X.  QQ ) )
109fveq2i 5706 . . . . . . . 8  |-  ( topGen `  B )  =  (
topGen `  ( (,) " ( QQ  X.  QQ ) ) )
1110tgqioo 20389 . . . . . . 7  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  B )
1211, 11oveq12i 6115 . . . . . 6  |-  ( (
topGen `  ran  (,) )  tX  ( topGen `  ran  (,) )
)  =  ( (
topGen `  B )  tX  ( topGen `  B )
)
13 qtopbas 20350 . . . . . . . 8  |-  ( (,) " ( QQ  X.  QQ ) )  e.  TopBases
149, 13eqeltri 2513 . . . . . . 7  |-  B  e.  TopBases
15 txbasval 19191 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  B  e. 
TopBases )  ->  ( ( topGen `
 B )  tX  ( topGen `  B )
)  =  ( B 
tX  B ) )
1614, 14, 15mp2an 672 . . . . . 6  |-  ( (
topGen `  B )  tX  ( topGen `  B )
)  =  ( B 
tX  B )
17 mbfimaopn.4 . . . . . . . 8  |-  K  =  ran  ( x  e.  B ,  y  e.  B  |->  ( x  X.  y ) )
1817txval 19149 . . . . . . 7  |-  ( ( B  e.  TopBases  /\  B  e. 
TopBases )  ->  ( B  tX  B )  =  (
topGen `  K ) )
1914, 14, 18mp2an 672 . . . . . 6  |-  ( B 
tX  B )  =  ( topGen `  K )
2012, 16, 193eqtri 2467 . . . . 5  |-  ( (
topGen `  ran  (,) )  tX  ( topGen `  ran  (,) )
)  =  ( topGen `  K )
218, 20syl6eleq 2533 . . . 4  |-  ( A  e.  J  ->  ( `' G " A )  e.  ( topGen `  K
) )
2217txbas 19152 . . . . . 6  |-  ( ( B  e.  TopBases  /\  B  e. 
TopBases )  ->  K  e.  TopBases )
2314, 14, 22mp2an 672 . . . . 5  |-  K  e.  TopBases
24 eltg3 18579 . . . . 5  |-  ( K  e.  TopBases  ->  ( ( `' G " A )  e.  ( topGen `  K
)  <->  E. t ( t 
C_  K  /\  ( `' G " A )  =  U. t ) ) )
2523, 24ax-mp 5 . . . 4  |-  ( ( `' G " A )  e.  ( topGen `  K
)  <->  E. t ( t 
C_  K  /\  ( `' G " A )  =  U. t ) )
2621, 25sylib 196 . . 3  |-  ( A  e.  J  ->  E. t
( t  C_  K  /\  ( `' G " A )  =  U. t ) )
2726adantl 466 . 2  |-  ( ( F  e. MblFn  /\  A  e.  J )  ->  E. t
( t  C_  K  /\  ( `' G " A )  =  U. t ) )
281cnref1o 10998 . . . . . . . 8  |-  G :
( RR  X.  RR )
-1-1-onto-> CC
29 f1ofo 5660 . . . . . . . 8  |-  ( G : ( RR  X.  RR ) -1-1-onto-> CC  ->  G :
( RR  X.  RR ) -onto-> CC )
3028, 29ax-mp 5 . . . . . . 7  |-  G :
( RR  X.  RR ) -onto-> CC
31 elssuni 4133 . . . . . . . . 9  |-  ( A  e.  J  ->  A  C_ 
U. J )
323cnfldtopon 20374 . . . . . . . . . 10  |-  J  e.  (TopOn `  CC )
3332toponunii 18549 . . . . . . . . 9  |-  CC  =  U. J
3431, 33syl6sseqr 3415 . . . . . . . 8  |-  ( A  e.  J  ->  A  C_  CC )
3534ad2antlr 726 . . . . . . 7  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  A  C_  CC )
36 foimacnv 5670 . . . . . . 7  |-  ( ( G : ( RR 
X.  RR ) -onto-> CC 
/\  A  C_  CC )  ->  ( G "
( `' G " A ) )  =  A )
3730, 35, 36sylancr 663 . . . . . 6  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  ( G " ( `' G " A ) )  =  A )
38 simprr 756 . . . . . . . 8  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  ( `' G " A )  = 
U. t )
3938imaeq2d 5181 . . . . . . 7  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  ( G " ( `' G " A ) )  =  ( G " U. t ) )
40 imauni 5975 . . . . . . 7  |-  ( G
" U. t )  =  U_ w  e.  t  ( G "
w )
4139, 40syl6eq 2491 . . . . . 6  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  ( G " ( `' G " A ) )  = 
U_ w  e.  t  ( G " w
) )
4237, 41eqtr3d 2477 . . . . 5  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  A  =  U_ w  e.  t  ( G " w ) )
4342imaeq2d 5181 . . . 4  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  ( `' F " A )  =  ( `' F " U_ w  e.  t 
( G " w
) ) )
44 imaiun 5974 . . . 4  |-  ( `' F " U_ w  e.  t  ( G " w ) )  = 
U_ w  e.  t  ( `' F "
( G " w
) )
4543, 44syl6eq 2491 . . 3  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  ( `' F " A )  = 
U_ w  e.  t  ( `' F "
( G " w
) ) )
46 ssdomg 7367 . . . . . . 7  |-  ( K  e.  TopBases  ->  ( t  C_  K  ->  t  ~<_  K ) )
4723, 46ax-mp 5 . . . . . 6  |-  ( t 
C_  K  ->  t  ~<_  K )
48 omelon 7864 . . . . . . . . . . 11  |-  om  e.  On
49 nnenom 11814 . . . . . . . . . . . 12  |-  NN  ~~  om
5049ensymi 7371 . . . . . . . . . . 11  |-  om  ~~  NN
51 isnumi 8128 . . . . . . . . . . 11  |-  ( ( om  e.  On  /\  om 
~~  NN )  ->  NN  e.  dom  card )
5248, 50, 51mp2an 672 . . . . . . . . . 10  |-  NN  e.  dom  card
53 qnnen 13508 . . . . . . . . . . . . . . . . . . . 20  |-  QQ  ~~  NN
54 xpen 7486 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( QQ  ~~  NN  /\  QQ  ~~  NN )  -> 
( QQ  X.  QQ )  ~~  ( NN  X.  NN ) )
5553, 53, 54mp2an 672 . . . . . . . . . . . . . . . . . . 19  |-  ( QQ 
X.  QQ )  ~~  ( NN  X.  NN )
56 xpnnen 13503 . . . . . . . . . . . . . . . . . . 19  |-  ( NN 
X.  NN )  ~~  NN
5755, 56entri 7375 . . . . . . . . . . . . . . . . . 18  |-  ( QQ 
X.  QQ )  ~~  NN
5857, 49entr2i 7376 . . . . . . . . . . . . . . . . 17  |-  om  ~~  ( QQ  X.  QQ )
59 isnumi 8128 . . . . . . . . . . . . . . . . 17  |-  ( ( om  e.  On  /\  om 
~~  ( QQ  X.  QQ ) )  ->  ( QQ  X.  QQ )  e. 
dom  card )
6048, 58, 59mp2an 672 . . . . . . . . . . . . . . . 16  |-  ( QQ 
X.  QQ )  e. 
dom  card
61 ioof 11399 . . . . . . . . . . . . . . . . . 18  |-  (,) :
( RR*  X.  RR* ) --> ~P RR
62 ffun 5573 . . . . . . . . . . . . . . . . . 18  |-  ( (,)
: ( RR*  X.  RR* )
--> ~P RR  ->  Fun  (,) )
6361, 62ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  Fun  (,)
64 qssre 10975 . . . . . . . . . . . . . . . . . . . 20  |-  QQ  C_  RR
65 ressxr 9439 . . . . . . . . . . . . . . . . . . . 20  |-  RR  C_  RR*
6664, 65sstri 3377 . . . . . . . . . . . . . . . . . . 19  |-  QQ  C_  RR*
67 xpss12 4957 . . . . . . . . . . . . . . . . . . 19  |-  ( ( QQ  C_  RR*  /\  QQ  C_ 
RR* )  ->  ( QQ  X.  QQ )  C_  ( RR*  X.  RR* )
)
6866, 66, 67mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  ( QQ 
X.  QQ )  C_  ( RR*  X.  RR* )
6961fdmi 5576 . . . . . . . . . . . . . . . . . 18  |-  dom  (,)  =  ( RR*  X.  RR* )
7068, 69sseqtr4i 3401 . . . . . . . . . . . . . . . . 17  |-  ( QQ 
X.  QQ )  C_  dom  (,)
71 fores 5641 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  (,)  /\  ( QQ  X.  QQ )  C_  dom  (,) )  ->  ( (,)  |`  ( QQ  X.  QQ ) ) : ( QQ  X.  QQ )
-onto-> ( (,) " ( QQ  X.  QQ ) ) )
7263, 70, 71mp2an 672 . . . . . . . . . . . . . . . 16  |-  ( (,)  |`  ( QQ  X.  QQ ) ) : ( QQ  X.  QQ )
-onto-> ( (,) " ( QQ  X.  QQ ) )
73 fodomnum 8239 . . . . . . . . . . . . . . . 16  |-  ( ( QQ  X.  QQ )  e.  dom  card  ->  ( ( (,)  |`  ( QQ  X.  QQ ) ) : ( QQ  X.  QQ ) -onto-> ( (,) " ( QQ  X.  QQ ) )  ->  ( (,) " ( QQ  X.  QQ ) )  ~<_  ( QQ  X.  QQ ) ) )
7460, 72, 73mp2 9 . . . . . . . . . . . . . . 15  |-  ( (,) " ( QQ  X.  QQ ) )  ~<_  ( QQ 
X.  QQ )
759, 74eqbrtri 4323 . . . . . . . . . . . . . 14  |-  B  ~<_  ( QQ  X.  QQ )
76 domentr 7380 . . . . . . . . . . . . . 14  |-  ( ( B  ~<_  ( QQ  X.  QQ )  /\  ( QQ  X.  QQ )  ~~  NN )  ->  B  ~<_  NN )
7775, 57, 76mp2an 672 . . . . . . . . . . . . 13  |-  B  ~<_  NN
7814elexi 2994 . . . . . . . . . . . . . 14  |-  B  e. 
_V
7978xpdom1 7422 . . . . . . . . . . . . 13  |-  ( B  ~<_  NN  ->  ( B  X.  B )  ~<_  ( NN 
X.  B ) )
8077, 79ax-mp 5 . . . . . . . . . . . 12  |-  ( B  X.  B )  ~<_  ( NN  X.  B )
81 nnex 10340 . . . . . . . . . . . . . 14  |-  NN  e.  _V
8281xpdom2 7418 . . . . . . . . . . . . 13  |-  ( B  ~<_  NN  ->  ( NN  X.  B )  ~<_  ( NN 
X.  NN ) )
8377, 82ax-mp 5 . . . . . . . . . . . 12  |-  ( NN 
X.  B )  ~<_  ( NN  X.  NN )
84 domtr 7374 . . . . . . . . . . . 12  |-  ( ( ( B  X.  B
)  ~<_  ( NN  X.  B )  /\  ( NN  X.  B )  ~<_  ( NN  X.  NN ) )  ->  ( B  X.  B )  ~<_  ( NN 
X.  NN ) )
8580, 83, 84mp2an 672 . . . . . . . . . . 11  |-  ( B  X.  B )  ~<_  ( NN  X.  NN )
86 domentr 7380 . . . . . . . . . . 11  |-  ( ( ( B  X.  B
)  ~<_  ( NN  X.  NN )  /\  ( NN  X.  NN )  ~~  NN )  ->  ( B  X.  B )  ~<_  NN )
8785, 56, 86mp2an 672 . . . . . . . . . 10  |-  ( B  X.  B )  ~<_  NN
88 numdom 8220 . . . . . . . . . 10  |-  ( ( NN  e.  dom  card  /\  ( B  X.  B
)  ~<_  NN )  -> 
( B  X.  B
)  e.  dom  card )
8952, 87, 88mp2an 672 . . . . . . . . 9  |-  ( B  X.  B )  e. 
dom  card
90 eqid 2443 . . . . . . . . . . 11  |-  ( x  e.  B ,  y  e.  B  |->  ( x  X.  y ) )  =  ( x  e.  B ,  y  e.  B  |->  ( x  X.  y ) )
91 vex 2987 . . . . . . . . . . . 12  |-  x  e. 
_V
92 vex 2987 . . . . . . . . . . . 12  |-  y  e. 
_V
9391, 92xpex 6520 . . . . . . . . . . 11  |-  ( x  X.  y )  e. 
_V
9490, 93fnmpt2i 6655 . . . . . . . . . 10  |-  ( x  e.  B ,  y  e.  B  |->  ( x  X.  y ) )  Fn  ( B  X.  B )
95 dffn4 5638 . . . . . . . . . 10  |-  ( ( 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 ) ) )
9694, 95mpbi 208 . . . . . . . . 9  |-  ( 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 8239 . . . . . . . . 9  |-  ( ( 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 ) ) )
9889, 96, 97mp2 9 . . . . . . . 8  |-  ran  (
x  e.  B , 
y  e.  B  |->  ( x  X.  y ) )  ~<_  ( B  X.  B )
99 domtr 7374 . . . . . . . 8  |-  ( ( 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 )
10098, 87, 99mp2an 672 . . . . . . 7  |-  ran  (
x  e.  B , 
y  e.  B  |->  ( x  X.  y ) )  ~<_  NN
10117, 100eqbrtri 4323 . . . . . 6  |-  K  ~<_  NN
102 domtr 7374 . . . . . 6  |-  ( ( t  ~<_  K  /\  K  ~<_  NN )  ->  t  ~<_  NN )
10347, 101, 102sylancl 662 . . . . 5  |-  ( t 
C_  K  ->  t  ~<_  NN )
104103ad2antrl 727 . . . 4  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  t  ~<_  NN )
10517eleq2i 2507 . . . . . . . . 9  |-  ( w  e.  K  <->  w  e.  ran  ( x  e.  B ,  y  e.  B  |->  ( x  X.  y
) ) )
10690, 93elrnmpt2 6215 . . . . . . . . 9  |-  ( w  e.  ran  ( x  e.  B ,  y  e.  B  |->  ( x  X.  y ) )  <->  E. x  e.  B  E. y  e.  B  w  =  ( x  X.  y ) )
107105, 106bitri 249 . . . . . . . 8  |-  ( w  e.  K  <->  E. x  e.  B  E. y  e.  B  w  =  ( x  X.  y
) )
108 elin 3551 . . . . . . . . . . . . 13  |-  ( 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 21117 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  e. MblFn  ->  F : dom  F --> CC )
110109adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  F : dom  F --> CC )
111 fvco3 5780 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : dom  F --> CC  /\  z  e.  dom  F )  ->  ( (
Re  o.  F ) `  z )  =  ( Re `  ( F `
 z ) ) )
112110, 111sylan 471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  /\  z  e.  dom  F )  ->  (
( Re  o.  F
) `  z )  =  ( Re `  ( F `  z ) ) )
113112eleq1d 2509 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 5780 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : dom  F --> CC  /\  z  e.  dom  F )  ->  ( (
Im  o.  F ) `  z )  =  ( Im `  ( F `
 z ) ) )
115110, 114sylan 471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  /\  z  e.  dom  F )  ->  (
( Im  o.  F
) `  z )  =  ( Im `  ( F `  z ) ) )
116115eleq1d 2509 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  /\  z  e.  dom  F )  ->  (
( ( Im  o.  F ) `  z
)  e.  y  <->  ( Im `  ( F `  z
) )  e.  y ) )
117113, 116anbi12d 710 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
118110ffvelrnda 5855 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  /\  z  e.  dom  F )  ->  ( F `  z )  e.  CC )
119 fveq2 5703 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  ( F `  z )  ->  (
Re `  w )  =  ( Re `  ( F `  z ) ) )
120 fveq2 5703 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  ( F `  z )  ->  (
Im `  w )  =  ( Im `  ( F `  z ) ) )
121119, 120opeq12d 4079 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  ( F `  z )  ->  <. (
Re `  w ) ,  ( Im `  w ) >.  =  <. ( Re `  ( F `
 z ) ) ,  ( Im `  ( F `  z ) ) >. )
1221cnrecnv 12666 . . . . . . . . . . . . . . . . . . . . 21  |-  `' G  =  ( w  e.  CC  |->  <. ( Re `  w ) ,  ( Im `  w )
>. )
123 opex 4568 . . . . . . . . . . . . . . . . . . . . 21  |-  <. (
Re `  ( F `  z ) ) ,  ( Im `  ( F `  z )
) >.  e.  _V
124121, 122, 123fvmpt 5786 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  z )  e.  CC  ->  ( `' G `  ( F `
 z ) )  =  <. ( Re `  ( F `  z ) ) ,  ( Im
`  ( F `  z ) ) >.
)
125118, 124syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  /\  z  e.  dom  F )  ->  ( `' G `  ( F `
 z ) )  =  <. ( Re `  ( F `  z ) ) ,  ( Im
`  ( F `  z ) ) >.
)
126125eleq1d 2509 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) )
127118biantrurd 508 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) )
128126, 127bitr3d 255 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 4881 . . . . . . . . . . . . . . . . 17  |-  ( <.
( Re `  ( F `  z )
) ,  ( Im
`  ( F `  z ) ) >.  e.  ( x  X.  y
)  <->  ( ( Re
`  ( F `  z ) )  e.  x  /\  ( Im
`  ( F `  z ) )  e.  y ) )
130 f1ocnv 5665 . . . . . . . . . . . . . . . . . . . 20  |-  ( G : ( RR  X.  RR ) -1-1-onto-> CC  ->  `' G : CC -1-1-onto-> ( RR  X.  RR ) )
131 f1ofn 5654 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' G : CC -1-1-onto-> ( RR  X.  RR )  ->  `' G  Fn  CC )
13228, 130, 131mp2b 10 . . . . . . . . . . . . . . . . . . 19  |-  `' G  Fn  CC
133 elpreima 5835 . . . . . . . . . . . . . . . . . . 19  |-  ( `' G  Fn  CC  ->  ( ( F `  z
)  e.  ( `' `' G " ( x  X.  y ) )  <-> 
( ( F `  z )  e.  CC  /\  ( `' G `  ( F `  z ) )  e.  ( x  X.  y ) ) ) )
134132, 133ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  z )  e.  ( `' `' G " ( x  X.  y ) )  <->  ( ( F `  z )  e.  CC  /\  ( `' G `  ( F `
 z ) )  e.  ( x  X.  y ) ) )
135 imacnvcnv 5315 . . . . . . . . . . . . . . . . . . 19  |-  ( `' `' G " ( x  X.  y ) )  =  ( G "
( x  X.  y
) )
136135eleq2i 2507 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  z )  e.  ( `' `' G " ( x  X.  y ) )  <->  ( F `  z )  e.  ( G " ( x  X.  y ) ) )
137134, 136bitr3i 251 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  z
)  e.  CC  /\  ( `' G `  ( F `
 z ) )  e.  ( x  X.  y ) )  <->  ( F `  z )  e.  ( G " ( x  X.  y ) ) )
138128, 129, 1373bitr3g 287 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
139117, 138bitrd 253 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
140139pm5.32da 641 . . . . . . . . . . . . . 14  |-  ( ( 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 12613 . . . . . . . . . . . . . . . . . . 19  |-  Re : CC
--> RR
142 fco 5580 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Re : CC --> RR  /\  F : dom  F --> CC )  ->  ( Re  o.  F ) : dom  F --> RR )
143141, 109, 142sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( F  e. MblFn  ->  ( Re  o.  F ) : dom  F --> RR )
144 ffn 5571 . . . . . . . . . . . . . . . . . 18  |-  ( ( Re  o.  F ) : dom  F --> RR  ->  ( Re  o.  F )  Fn  dom  F )
145 elpreima 5835 . . . . . . . . . . . . . . . . . 18  |-  ( ( Re  o.  F )  Fn  dom  F  -> 
( z  e.  ( `' ( Re  o.  F ) " x
)  <->  ( z  e. 
dom  F  /\  (
( Re  o.  F
) `  z )  e.  x ) ) )
146143, 144, 1453syl 20 . . . . . . . . . . . . . . . . 17  |-  ( F  e. MblFn  ->  ( z  e.  ( `' ( Re  o.  F ) "
x )  <->  ( z  e.  dom  F  /\  (
( Re  o.  F
) `  z )  e.  x ) ) )
147 imf 12614 . . . . . . . . . . . . . . . . . . 19  |-  Im : CC
--> RR
148 fco 5580 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Im : CC --> RR  /\  F : dom  F --> CC )  ->  ( Im  o.  F ) : dom  F --> RR )
149147, 109, 148sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( F  e. MblFn  ->  ( Im  o.  F ) : dom  F --> RR )
150 ffn 5571 . . . . . . . . . . . . . . . . . 18  |-  ( ( Im  o.  F ) : dom  F --> RR  ->  ( Im  o.  F )  Fn  dom  F )
151 elpreima 5835 . . . . . . . . . . . . . . . . . 18  |-  ( ( Im  o.  F )  Fn  dom  F  -> 
( z  e.  ( `' ( Im  o.  F ) " y
)  <->  ( z  e. 
dom  F  /\  (
( Im  o.  F
) `  z )  e.  y ) ) )
152149, 150, 1513syl 20 . . . . . . . . . . . . . . . . 17  |-  ( F  e. MblFn  ->  ( z  e.  ( `' ( Im  o.  F ) "
y )  <->  ( z  e.  dom  F  /\  (
( Im  o.  F
) `  z )  e.  y ) ) )
153146, 152anbi12d 710 . . . . . . . . . . . . . . . 16  |-  ( 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 824 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) )
155153, 154syl6bbr 263 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
156155adantr 465 . . . . . . . . . . . . . 14  |-  ( ( 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 5571 . . . . . . . . . . . . . . . 16  |-  ( F : dom  F --> CC  ->  F  Fn  dom  F )
158 elpreima 5835 . . . . . . . . . . . . . . . 16  |-  ( F  Fn  dom  F  -> 
( z  e.  ( `' F " ( G
" ( x  X.  y ) ) )  <-> 
( z  e.  dom  F  /\  ( F `  z )  e.  ( G " ( x  X.  y ) ) ) ) )
159109, 157, 1583syl 20 . . . . . . . . . . . . . . 15  |-  ( F  e. MblFn  ->  ( z  e.  ( `' F "
( G " (
x  X.  y ) ) )  <->  ( z  e.  dom  F  /\  ( F `  z )  e.  ( G " (
x  X.  y ) ) ) ) )
160159adantr 465 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) ) ) )
161140, 156, 1603bitr4d 285 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) ) )
162108, 161syl5bb 257 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) ) )
163162eqrdv 2441 . . . . . . . . . . 11  |-  ( ( 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 21121 . . . . . . . . . . . . . . . . . 18  |-  ( F : dom  F --> CC  ->  ( F  e. MblFn  <->  ( ( Re  o.  F )  e. MblFn  /\  ( Im  o.  F
)  e. MblFn ) )
)
165109, 164syl 16 . . . . . . . . . . . . . . . . 17  |-  ( F  e. MblFn  ->  ( F  e. MblFn  <->  ( ( Re  o.  F
)  e. MblFn  /\  (
Im  o.  F )  e. MblFn ) ) )
166165ibi 241 . . . . . . . . . . . . . . . 16  |-  ( F  e. MblFn  ->  ( ( Re  o.  F )  e. MblFn  /\  ( Im  o.  F
)  e. MblFn ) )
167166simpld 459 . . . . . . . . . . . . . . 15  |-  ( F  e. MblFn  ->  ( Re  o.  F )  e. MblFn )
168 ismbf 21120 . . . . . . . . . . . . . . . 16  |-  ( ( Re  o.  F ) : dom  F --> RR  ->  ( ( Re  o.  F
)  e. MblFn  <->  A. x  e.  ran  (,) ( `' ( Re  o.  F ) "
x )  e.  dom  vol ) )
169143, 168syl 16 . . . . . . . . . . . . . . 15  |-  ( F  e. MblFn  ->  ( ( Re  o.  F )  e. MblFn  <->  A. x  e.  ran  (,) ( `' ( Re  o.  F ) " x
)  e.  dom  vol ) )
170167, 169mpbid 210 . . . . . . . . . . . . . 14  |-  ( F  e. MblFn  ->  A. x  e.  ran  (,) ( `' ( Re  o.  F ) "
x )  e.  dom  vol )
171170adantr 465 . . . . . . . . . . . . 13  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  A. x  e.  ran  (,) ( `' ( Re  o.  F
) " x )  e.  dom  vol )
172 imassrn 5192 . . . . . . . . . . . . . . 15  |-  ( (,) " ( QQ  X.  QQ ) )  C_  ran  (,)
1739, 172eqsstri 3398 . . . . . . . . . . . . . 14  |-  B  C_  ran  (,)
174 simprl 755 . . . . . . . . . . . . . 14  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  x  e.  B )
175173, 174sseldi 3366 . . . . . . . . . . . . 13  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  x  e.  ran  (,) )
176 rsp 2788 . . . . . . . . . . . . 13  |-  ( A. x  e.  ran  (,) ( `' ( Re  o.  F ) " x
)  e.  dom  vol  ->  ( x  e.  ran  (,) 
->  ( `' ( Re  o.  F ) "
x )  e.  dom  vol ) )
177171, 175, 176sylc 60 . . . . . . . . . . . 12  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  ( `' ( Re  o.  F
) " x )  e.  dom  vol )
178166simprd 463 . . . . . . . . . . . . . . 15  |-  ( F  e. MblFn  ->  ( Im  o.  F )  e. MblFn )
179 ismbf 21120 . . . . . . . . . . . . . . . 16  |-  ( ( Im  o.  F ) : dom  F --> RR  ->  ( ( Im  o.  F
)  e. MblFn  <->  A. y  e.  ran  (,) ( `' ( Im  o.  F ) "
y )  e.  dom  vol ) )
180149, 179syl 16 . . . . . . . . . . . . . . 15  |-  ( F  e. MblFn  ->  ( ( Im  o.  F )  e. MblFn  <->  A. y  e.  ran  (,) ( `' ( Im  o.  F ) " y
)  e.  dom  vol ) )
181178, 180mpbid 210 . . . . . . . . . . . . . 14  |-  ( F  e. MblFn  ->  A. y  e.  ran  (,) ( `' ( Im  o.  F ) "
y )  e.  dom  vol )
182181adantr 465 . . . . . . . . . . . . 13  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  A. y  e.  ran  (,) ( `' ( Im  o.  F
) " y )  e.  dom  vol )
183 simprr 756 . . . . . . . . . . . . . 14  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  y  e.  B )
184173, 183sseldi 3366 . . . . . . . . . . . . 13  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  y  e.  ran  (,) )
185 rsp 2788 . . . . . . . . . . . . 13  |-  ( A. y  e.  ran  (,) ( `' ( Im  o.  F ) " y
)  e.  dom  vol  ->  ( y  e.  ran  (,) 
->  ( `' ( Im  o.  F ) "
y )  e.  dom  vol ) )
186182, 184, 185sylc 60 . . . . . . . . . . . 12  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  ( `' ( Im  o.  F
) " y )  e.  dom  vol )
187 inmbl 21035 . . . . . . . . . . . 12  |-  ( ( ( `' ( 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 )
188177, 186, 187syl2anc 661 . . . . . . . . . . 11  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  ( ( `' ( Re  o.  F ) " x
)  i^i  ( `' ( Im  o.  F
) " y ) )  e.  dom  vol )
189163, 188eqeltrrd 2518 . . . . . . . . . 10  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  ( `' F " ( G "
( x  X.  y
) ) )  e. 
dom  vol )
190 imaeq2 5177 . . . . . . . . . . . 12  |-  ( w  =  ( x  X.  y )  ->  ( G " w )  =  ( G " (
x  X.  y ) ) )
191190imaeq2d 5181 . . . . . . . . . . 11  |-  ( w  =  ( x  X.  y )  ->  ( `' F " ( G
" w ) )  =  ( `' F " ( G " (
x  X.  y ) ) ) )
192191eleq1d 2509 . . . . . . . . . 10  |-  ( w  =  ( x  X.  y )  ->  (
( `' F "
( G " w
) )  e.  dom  vol  <->  ( `' F " ( G
" ( x  X.  y ) ) )  e.  dom  vol )
)
193189, 192syl5ibrcom 222 . . . . . . . . 9  |-  ( ( F  e. MblFn  /\  (
x  e.  B  /\  y  e.  B )
)  ->  ( w  =  ( x  X.  y )  ->  ( `' F " ( G
" w ) )  e.  dom  vol )
)
194193rexlimdvva 2860 . . . . . . . 8  |-  ( F  e. MblFn  ->  ( E. x  e.  B  E. y  e.  B  w  =  ( x  X.  y
)  ->  ( `' F " ( G "
w ) )  e. 
dom  vol ) )
195107, 194syl5bi 217 . . . . . . 7  |-  ( F  e. MblFn  ->  ( w  e.  K  ->  ( `' F " ( G "
w ) )  e. 
dom  vol ) )
196195ralrimiv 2810 . . . . . 6  |-  ( F  e. MblFn  ->  A. w  e.  K  ( `' F " ( G
" w ) )  e.  dom  vol )
197 ssralv 3428 . . . . . 6  |-  ( t 
C_  K  ->  ( A. w  e.  K  ( `' F " ( G
" w ) )  e.  dom  vol  ->  A. w  e.  t  ( `' F " ( G
" w ) )  e.  dom  vol )
)
198196, 197mpan9 469 . . . . 5  |-  ( ( F  e. MblFn  /\  t  C_  K )  ->  A. w  e.  t  ( `' F " ( G "
w ) )  e. 
dom  vol )
199198ad2ant2r 746 . . . 4  |-  ( ( ( 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 21050 . . . 4  |-  ( ( t  ~<_  NN  /\  A. w  e.  t  ( `' F " ( G "
w ) )  e. 
dom  vol )  ->  U_ w  e.  t  ( `' F " ( G "
w ) )  e. 
dom  vol )
201104, 199, 200syl2anc 661 . . 3  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  U_ w  e.  t  ( `' F " ( G " w
) )  e.  dom  vol )
20245, 201eqeltrd 2517 . 2  |-  ( ( ( F  e. MblFn  /\  A  e.  J )  /\  (
t  C_  K  /\  ( `' G " A )  =  U. t ) )  ->  ( `' F " A )  e. 
dom  vol )
20327, 202exlimddv 1692 1  |-  ( ( F  e. MblFn  /\  A  e.  J )  ->  ( `' F " A )  e.  dom  vol )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   A.wral 2727   E.wrex 2728    i^i cin 3339    C_ wss 3340   ~Pcpw 3872   <.cop 3895   U.cuni 4103   U_ciun 4183   class class class wbr 4304   Oncon0 4731    X. cxp 4850   `'ccnv 4851   dom cdm 4852   ran crn 4853    |` cres 4854   "cima 4855    o. ccom 4856   Fun wfun 5424    Fn wfn 5425   -->wf 5426   -onto->wfo 5428   -1-1-onto->wf1o 5429   ` cfv 5430  (class class class)co 6103    e. cmpt2 6105   omcom 6488    ~~ cen 7319    ~<_ cdom 7320   cardccrd 8117   CCcc 9292   RRcr 9293   _ici 9296    + caddc 9297    x. cmul 9299   RR*cxr 9429   NNcn 10334   QQcq 10965   (,)cioo 11312   Recre 12598   Imcim 12599   TopOpenctopn 14372   topGenctg 14388  ℂfldccnfld 17830   TopBasesctb 18514    Cn ccn 18840    tX ctx 19145   Homeochmeo 19338   volcvol 20959  MblFncmbf 21106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-inf2 7859  ax-cc 8616  ax-cnex 9350  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1 9362  ax-1ne0 9363  ax-1rid 9364  ax-rnegex 9365  ax-rrecex 9366  ax-cnre 9367  ax-pre-lttri 9368  ax-pre-lttrn 9369  ax-pre-ltadd 9370  ax-pre-mulgt0 9371  ax-pre-sup 9372  ax-addf 9373  ax-mulf 9374
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rmo 2735  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-pss 3356  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-tp 3894  df-op 3896  df-uni 4104  df-int 4141  df-iun 4185  df-iin 4186  df-disj 4275  df-br 4305  df-opab 4363  df-mpt 4364  df-tr 4398  df-eprel 4644  df-id 4648  df-po 4653  df-so 4654  df-fr 4691  df-se 4692  df-we 4693  df-ord 4734  df-on 4735  df-lim 4736  df-suc 4737  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-isom 5439  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-of 6332  df-om 6489  df-1st 6589  df-2nd 6590  df-supp 6703  df-recs 6844  df-rdg 6878  df-1o 6932  df-2o 6933  df-oadd 6936  df-omul 6937  df-er 7113  df-map 7228  df-pm 7229  df-ixp 7276  df-en 7323  df-dom 7324  df-sdom 7325  df-fin 7326  df-fsupp 7633  df-fi 7673  df-sup 7703  df-oi 7736  df-card 8121  df-acn 8124  df-cda 8349  df-pnf 9432  df-mnf 9433  df-xr 9434  df-ltxr 9435  df-le 9436  df-sub 9609  df-neg 9610  df-div 10006  df-nn 10335  df-2 10392  df-3 10393  df-4 10394  df-5 10395  df-6 10396  df-7 10397  df-8 10398  df-9 10399  df-10 10400  df-n0 10592  df-z 10659  df-dec 10768  df-uz 10874  df-q 10966  df-rp 11004  df-xneg 11101  df-xadd 11102  df-xmul 11103  df-ioo 11316  df-ico 11318  df-icc 11319  df-fz 11450  df-fzo 11561  df-fl 11654  df-seq 11819  df-exp 11878  df-hash 12116  df-cj 12600  df-re 12601  df-im 12602  df-sqr 12736  df-abs 12737  df-clim 12978  df-rlim 12979  df-sum 13176  df-struct 14188  df-ndx 14189  df-slot 14190  df-base 14191  df-sets 14192  df-ress 14193  df-plusg 14263  df-mulr 14264  df-starv 14265  df-sca 14266  df-vsca 14267  df-ip 14268  df-tset 14269  df-ple 14270  df-ds 14272  df-unif 14273  df-hom 14274  df-cco 14275  df-rest 14373  df-topn 14374  df-0g 14392  df-gsum 14393  df-topgen 14394  df-pt 14395  df-prds 14398  df-xrs 14452  df-qtop 14457  df-imas 14458  df-xps 14460  df-mre 14536  df-mrc 14537  df-acs 14539  df-mnd 15427  df-submnd 15477  df-mulg 15560  df-cntz 15847  df-cmn 16291  df-psmet 17821  df-xmet 17822  df-met 17823  df-bl 17824  df-mopn 17825  df-cnfld 17831  df-top 18515  df-bases 18517  df-topon 18518  df-topsp 18519  df-cn 18843  df-cnp 18844  df-tx 19147  df-hmeo 19340  df-xms 19907  df-ms 19908  df-tms 19909  df-cncf 20466  df-ovol 20960  df-vol 20961  df-mbf 21111
This theorem is referenced by:  mbfimaopn  21146
  Copyright terms: Public domain W3C validator