MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrsmopn Structured version   Visualization version   Unicode version
Theorem xrsmopn 21879
Description: The metric on the extended reals generates a topology, but this does not match the order topology on RR*; for example { +oo } is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015.)
Hypotheses
Ref Expression
xrsxmet.1 |- D = ( dist ` RR*s )
xrsmopn.1 |- J = ( MetOpen ` D )
Assertion
Ref Expression
xrsmopn |- (ordTop ` <_ ) C_ J
Proof of Theorem xrsmopn
Dummy variables x r y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elssuni 4241 . . . 4 |- ( x e. (ordTop ` <_ ) -> x C_ U. (ordTop ` <_ ) )
2 letopuni 20272 . . . 4 |- RR* = U. (ordTop ` <_ )
31, 2syl6sseqr 3491 . . 3 |- ( x e. (ordTop ` <_ ) -> x C_ RR* )
4 eqid 2462 . . . . . . . . 9 |- ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
54rexmet 21858 . . . . . . . 8 |- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
65a1i 11 . . . . . . 7 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) )
7 letop 20271 . . . . . . . . 9 |- (ordTop ` <_ ) e. Top
8 reex 9656 . . . . . . . . 9 |- RR e. _V
9 elrestr 15376 . . . . . . . . 9 |- ( ( (ordTop ` <_ ) e. Top /\ RR e. _V /\ x e. (ordTop ` <_ ) ) -> ( x i^i RR ) e. ( (ordTop ` <_ ) ↾t RR ) )
107, 8, 9mp3an12 1363 . . . . . . . 8 |- ( x e. (ordTop ` <_ ) -> ( x i^i RR ) e. ( (ordTop ` <_ ) ↾t RR ) )
1110ad2antrr 737 . . . . . . 7 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> ( x i^i RR ) e. ( (ordTop ` <_ ) ↾t RR ) )
12 elin 3629 . . . . . . . . 9 |- ( y e. ( x i^i RR ) <-> ( y e. x /\ y e. RR ) )
1312biimpri 211 . . . . . . . 8 |- ( ( y e. x /\ y e. RR ) -> y e. ( x i^i RR ) )
1413adantll 725 . . . . . . 7 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> y e. ( x i^i RR ) )
15 eqid 2462 . . . . . . . . . 10 |- ( (ordTop ` <_ ) ↾t RR ) = ( (ordTop ` <_ ) ↾t RR )
1615xrtgioo 21873 . . . . . . . . 9 |- ( topGen ` ran (,) ) = ( (ordTop ` <_ ) ↾t RR )
17 eqid 2462 . . . . . . . . . 10 |- ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
184, 17tgioo 21863 . . . . . . . . 9 |- ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
1916, 18eqtr3i 2486 . . . . . . . 8 |- ( (ordTop ` <_ ) ↾t RR ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
2019mopni2 21557 . . . . . . 7 |- ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( x i^i RR ) e. ( (ordTop ` <_ ) ↾t RR ) /\ y e. ( x i^i RR ) ) -> E. r e. RR+ ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) )
216, 11, 14, 20syl3anc 1276 . . . . . 6 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> E. r e. RR+ ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) )
22 xrsxmet.1 . . . . . . . . . . . . 13 |- D = ( dist ` RR*s )
2322xrsxmet 21876 . . . . . . . . . . . 12 |- D e. ( *Met ` RR* )
2423a1i 11 . . . . . . . . . . 11 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> D e. ( *Met ` RR* ) )
25 simplr 767 . . . . . . . . . . . 12 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> y e. RR )
26 ressxr 9710 . . . . . . . . . . . . 13 |- RR C_ RR*
27 dfss1 3649 . . . . . . . . . . . . 13 |- ( RR C_ RR* <-> ( RR* i^i RR ) = RR )
2826, 27mpbi 213 . . . . . . . . . . . 12 |- ( RR* i^i RR ) = RR
2925, 28syl6eleqr 2551 . . . . . . . . . . 11 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> y e. ( RR* i^i RR ) )
30 rpxr 11338 . . . . . . . . . . . 12 |- ( r e. RR+ -> r e. RR* )
3130adantl 472 . . . . . . . . . . 11 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> r e. RR* )
3222xrsdsre 21877 . . . . . . . . . . . . 13 |- ( D |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
3332eqcomi 2471 . . . . . . . . . . . 12 |- ( ( abs o. - ) |` ( RR X. RR ) ) = ( D |` ( RR X. RR ) )
3433blres 21495 . . . . . . . . . . 11 |- ( ( D e. ( *Met ` RR* ) /\ y e. ( RR* i^i RR ) /\ r e. RR* ) -> ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( y ( ball ` D ) r ) i^i RR ) )
3524, 29, 31, 34syl3anc 1276 . . . . . . . . . 10 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( y ( ball ` D ) r ) i^i RR ) )
3622xrsblre 21878 . . . . . . . . . . . . 13 |- ( ( y e. RR /\ r e. RR* ) -> ( y ( ball ` D ) r ) C_ RR )
3730, 36sylan2 481 . . . . . . . . . . . 12 |- ( ( y e. RR /\ r e. RR+ ) -> ( y ( ball ` D ) r ) C_ RR )
3837adantll 725 . . . . . . . . . . 11 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( y ( ball ` D ) r ) C_ RR )
39 df-ss 3430 . . . . . . . . . . 11 |- ( ( y ( ball ` D ) r ) C_ RR <-> ( ( y ( ball ` D ) r ) i^i RR ) = ( y ( ball ` D ) r ) )
4038, 39sylib 201 . . . . . . . . . 10 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( ( y ( ball ` D ) r ) i^i RR ) = ( y ( ball ` D ) r ) )
4135, 40eqtrd 2496 . . . . . . . . 9 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( y ( ball ` D ) r ) )
4241sseq1d 3471 . . . . . . . 8 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) <-> ( y ( ball ` D ) r ) C_ ( x i^i RR ) ) )
43 inss1 3664 . . . . . . . . 9 |- ( x i^i RR ) C_ x
44 sstr 3452 . . . . . . . . 9 |- ( ( ( y ( ball ` D ) r ) C_ ( x i^i RR ) /\ ( x i^i RR ) C_ x ) -> ( y ( ball ` D ) r ) C_ x )
4543, 44mpan2 682 . . . . . . . 8 |- ( ( y ( ball ` D ) r ) C_ ( x i^i RR ) -> ( y ( ball ` D ) r ) C_ x )
4642, 45syl6bi 236 . . . . . . 7 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) -> ( y ( ball ` D ) r ) C_ x ) )
4746reximdva 2874 . . . . . 6 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> ( E. r e. RR+ ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) )
4821, 47mpd 15 . . . . 5 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
49 1rp 11335 . . . . . 6 |- 1 e. RR+
5023a1i 11 . . . . . . . . 9 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> D e. ( *Met ` RR* ) )
513sselda 3444 . . . . . . . . . 10 |- ( ( x e. (ordTop ` <_ ) /\ y e. x ) -> y e. RR* )
5251adantr 471 . . . . . . . . 9 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> y e. RR* )
53 rpxr 11338 . . . . . . . . . 10 |- ( 1 e. RR+ -> 1 e. RR* )
5449, 53mp1i 13 . . . . . . . . 9 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> 1 e. RR* )
55 elbl 21452 . . . . . . . . 9 |- ( ( D e. ( *Met ` RR* ) /\ y e. RR* /\ 1 e. RR* ) -> ( z e. ( y ( ball ` D ) 1 ) <-> ( z e. RR* /\ ( y D z ) < 1 ) ) )
5650, 52, 54, 55syl3anc 1276 . . . . . . . 8 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( z e. ( y ( ball ` D ) 1 ) <-> ( z e. RR* /\ ( y D z ) < 1 ) ) )
57 simp2 1015 . . . . . . . . . 10 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> -. y e. RR )
5823a1i 11 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> D e. ( *Met ` RR* ) )
59513ad2ant1 1035 . . . . . . . . . . . . . . . . . 18 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> y e. RR* )
6059adantr 471 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> y e. RR* )
61 simpl3l 1069 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> z e. RR* )
62 xmetcl 21395 . . . . . . . . . . . . . . . . 17 |- ( ( D e. ( *Met ` RR* ) /\ y e. RR* /\ z e. RR* ) -> ( y D z ) e. RR* )
6358, 60, 61, 62syl3anc 1276 . . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) e. RR* )
64 1red 9684 . . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> 1 e. RR )
65 xmetge0 21408 . . . . . . . . . . . . . . . . 17 |- ( ( D e. ( *Met ` RR* ) /\ y e. RR* /\ z e. RR* ) -> 0 <_ ( y D z ) )
6658, 60, 61, 65syl3anc 1276 . . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> 0 <_ ( y D z ) )
67 simpl3r 1070 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) < 1 )
6849, 53ax-mp 5 . . . . . . . . . . . . . . . . . 18 |- 1 e. RR*
69 xrltle 11477 . . . . . . . . . . . . . . . . . 18 |- ( ( ( y D z ) e. RR* /\ 1 e. RR* ) -> ( ( y D z ) < 1 -> ( y D z ) <_ 1 ) )
7063, 68, 69sylancl 673 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( ( y D z ) < 1 -> ( y D z ) <_ 1 ) )
7167, 70mpd 15 . . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) <_ 1 )
72 xrrege0 11498 . . . . . . . . . . . . . . . 16 |- ( ( ( ( y D z ) e. RR* /\ 1 e. RR ) /\ ( 0 <_ ( y D z ) /\ ( y D z ) <_ 1 ) ) -> ( y D z ) e. RR )
7363, 64, 66, 71, 72syl22anc 1277 . . . . . . . . . . . . . . 15 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) e. RR )
74 simpr 467 . . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> y =/= z )
7522xrsdsreclb 19064 . . . . . . . . . . . . . . . 16 |- ( ( y e. RR* /\ z e. RR* /\ y =/= z ) -> ( ( y D z ) e. RR <-> ( y e. RR /\ z e. RR ) ) )
7660, 61, 74, 75syl3anc 1276 . . . . . . . . . . . . . . 15 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( ( y D z ) e. RR <-> ( y e. RR /\ z e. RR ) ) )
7773, 76mpbid 215 . . . . . . . . . . . . . 14 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y e. RR /\ z e. RR ) )
7877simpld 465 . . . . . . . . . . . . 13 |- ( ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> y e. RR )
7978ex 440 . . . . . . . . . . . 12 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( y =/= z -> y e. RR ) )
8079necon1bd 2654 . . . . . . . . . . 11 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( -. y e. RR -> y = z ) )
81 simp1r 1039 . . . . . . . . . . . 12 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> y e. x )
82 elequ1 1905 . . . . . . . . . . . 12 |- ( y = z -> ( y e. x <-> z e. x ) )
8381, 82syl5ibcom 228 . . . . . . . . . . 11 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( y = z -> z e. x ) )
8480, 83syld 45 . . . . . . . . . 10 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( -. y e. RR -> z e. x ) )
8557, 84mpd 15 . . . . . . . . 9 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> z e. x )
86853expia 1217 . . . . . . . 8 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( ( z e. RR* /\ ( y D z ) < 1 ) -> z e. x ) )
8756, 86sylbid 223 . . . . . . 7 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( z e. ( y ( ball ` D ) 1 ) -> z e. x ) )
8887ssrdv 3450 . . . . . 6 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( y ( ball ` D ) 1 ) C_ x )
89 oveq2 6323 . . . . . . . 8 |- ( r = 1 -> ( y ( ball ` D ) r ) = ( y ( ball ` D ) 1 ) )
9089sseq1d 3471 . . . . . . 7 |- ( r = 1 -> ( ( y ( ball ` D ) r ) C_ x <-> ( y ( ball ` D ) 1 ) C_ x ) )
9190rspcev 3162 . . . . . 6 |- ( ( 1 e. RR+ /\ ( y ( ball ` D ) 1 ) C_ x ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
9249, 88, 91sylancr 674 . . . . 5 |- ( ( ( x e. (ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
9348, 92pm2.61dan 805 . . . 4 |- ( ( x e. (ordTop ` <_ ) /\ y e. x ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
9493ralrimiva 2814 . . 3 |- ( x e. (ordTop ` <_ ) -> A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
95 xrsmopn.1 . . . . 5 |- J = ( MetOpen ` D )
9695elmopn2 21509 . . . 4 |- ( D e. ( *Met ` RR* ) -> ( x e. J <-> ( x C_ RR* /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) ) )
9723, 96ax-mp 5 . . 3 |- ( x e. J <-> ( x C_ RR* /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) )
983, 94, 97sylanbrc 675 . 2 |- ( x e. (ordTop ` <_ ) -> x e. J )
9998ssriv 3448 1 |- (ordTop ` <_ ) C_ J
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057   i^i cin 3415   C_ wss 3416   U.cuni 4212   class class class wbr 4416   X. cxp 4851   ran crn 4854   |` cres 4855   o. ccom 4857   ` cfv 5601  (class class class)co 6315   RRcr 9564   0cc0 9565   1c1 9566   RR*cxr 9700   < clt 9701   <_ cle 9702   - cmin 9886   RR+crp 11331   (,)cioo 11664   abscabs 13346   distcds 15248   ↾t crest 15368   topGenctg 15385  ordTopcordt 15446   RR*scxrs 15447   *Metcxmt 19004   ballcbl 19006   MetOpencmopn 19009   Topctop 19966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-ec 7391  df-map 7500  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fi 7951  df-sup 7982  df-inf 7983  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-ioo 11668  df-ioc 11669  df-ico 11670  df-icc 11671  df-fz 11814  df-seq 12246  df-exp 12305  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-plusg 15252  df-mulr 15253  df-tset 15258  df-ple 15259  df-ds 15261  df-rest 15370  df-topgen 15391  df-ordt 15448  df-xrs 15449  df-ps 16495  df-tsr 16496  df-psmet 19011  df-xmet 19012  df-met 19013  df-bl 19014  df-mopn 19015  df-top 19970  df-bases 19971  df-topon 19972
This theorem is referenced by:  xmetdcn  21905
  Copyright terms: Public domain W3C validator