Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  istotbnd3 Structured version   Unicode version

Theorem istotbnd3 32061
 Description: A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.)
Assertion
Ref Expression
istotbnd3
Distinct variable groups:   ,,,   ,,,

Proof of Theorem istotbnd3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 istotbnd 32059 . 2
2 oveq1 6310 . . . . . . . . . . . 12
32eqeq2d 2437 . . . . . . . . . . 11
43ac6sfi 7819 . . . . . . . . . 10
54ex 436 . . . . . . . . 9
65ad2antlr 732 . . . . . . . 8
7 simprrl 773 . . . . . . . . . . . . 13
8 frn 5750 . . . . . . . . . . . . 13
97, 8syl 17 . . . . . . . . . . . 12
10 simplr 761 . . . . . . . . . . . . 13
11 ffn 5744 . . . . . . . . . . . . . . 15
127, 11syl 17 . . . . . . . . . . . . . 14
13 dffn4 5814 . . . . . . . . . . . . . 14
1412, 13sylib 200 . . . . . . . . . . . . 13
15 fofi 7864 . . . . . . . . . . . . 13
1610, 14, 15syl2anc 666 . . . . . . . . . . . 12
17 elfpw 7880 . . . . . . . . . . . 12
189, 16, 17sylanbrc 669 . . . . . . . . . . 11
192eleq2d 2493 . . . . . . . . . . . . . . . 16
2019rexrn 6037 . . . . . . . . . . . . . . 15
2112, 20syl 17 . . . . . . . . . . . . . 14
22 eliun 4302 . . . . . . . . . . . . . 14
23 eliun 4302 . . . . . . . . . . . . . 14
2421, 22, 233bitr4g 292 . . . . . . . . . . . . 13
2524eqrdv 2420 . . . . . . . . . . . 12
26 simprrr 774 . . . . . . . . . . . . 13
27 iuneq2 4314 . . . . . . . . . . . . 13
2826, 27syl 17 . . . . . . . . . . . 12
29 uniiun 4350 . . . . . . . . . . . . 13
30 simprl 763 . . . . . . . . . . . . 13
3129, 30syl5eqr 2478 . . . . . . . . . . . 12
3225, 28, 313eqtr2d 2470 . . . . . . . . . . 11
33 iuneq1 4311 . . . . . . . . . . . . 13
3433eqeq1d 2425 . . . . . . . . . . . 12
3534rspcev 3183 . . . . . . . . . . 11
3618, 32, 35syl2anc 666 . . . . . . . . . 10
3736expr 619 . . . . . . . . 9
3837exlimdv 1769 . . . . . . . 8
396, 38syld 46 . . . . . . 7
4039expimpd 607 . . . . . 6
4140rexlimdva 2918 . . . . 5
42 elfpw 7880 . . . . . . . . . . 11
4342simprbi 466 . . . . . . . . . 10
4443ad2antrl 733 . . . . . . . . 9
45 mptfi 7877 . . . . . . . . 9
46 rnfi 7861 . . . . . . . . 9
4744, 45, 463syl 18 . . . . . . . 8
48 ovex 6331 . . . . . . . . . 10
4948dfiun3 5106 . . . . . . . . 9
50 simprr 765 . . . . . . . . 9
5149, 50syl5eqr 2478 . . . . . . . 8
52 eqid 2423 . . . . . . . . . 10
5352rnmpt 5097 . . . . . . . . 9
5442simplbi 462 . . . . . . . . . . . 12
5554ad2antrl 733 . . . . . . . . . . 11
56 ssrexv 3527 . . . . . . . . . . 11
5755, 56syl 17 . . . . . . . . . 10
5857ss2abdv 3535 . . . . . . . . 9
5953, 58syl5eqss 3509 . . . . . . . 8
60 unieq 4225 . . . . . . . . . . 11
6160eqeq1d 2425 . . . . . . . . . 10
62 ssabral 3533 . . . . . . . . . . 11
63 sseq1 3486 . . . . . . . . . . 11
6462, 63syl5bbr 263 . . . . . . . . . 10
6561, 64anbi12d 716 . . . . . . . . 9
6665rspcev 3183 . . . . . . . 8
6747, 51, 59, 66syl12anc 1263 . . . . . . 7
6867expr 619 . . . . . 6
6968rexlimdva 2918 . . . . 5
7041, 69impbid 194 . . . 4
7170ralbidv 2865 . . 3
7271pm5.32i 642 . 2
731, 72bitri 253 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1438  wex 1660   wcel 1869  cab 2408  wral 2776  wrex 2777   cin 3436   wss 3437  cpw 3980  cuni 4217  ciun 4297   cmpt 4480   crn 4852   wfn 5594  wf 5595  wfo 5597  cfv 5599  (class class class)co 6303  cfn 7575  crp 11304  cme 18949  cbl 18950  ctotbnd 32056 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-oadd 7192  df-er 7369  df-en 7576  df-dom 7577  df-fin 7579  df-totbnd 32058 This theorem is referenced by:  0totbnd  32063  sstotbnd2  32064  equivtotbnd  32068  totbndbnd  32079  prdstotbnd  32084
 Copyright terms: Public domain W3C validator