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

Theorem fnex 5741
Description: If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 5737. See fnexALT 5742 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fnex  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  F  e.  _V )

Proof of Theorem fnex
StepHypRef Expression
1 fnrel 5342 . . 3  |-  ( F  Fn  A  ->  Rel  F )
21adantr 451 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  Rel  F )
3 df-fn 5258 . . 3  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 eleq1a 2352 . . . . . 6  |-  ( A  e.  B  ->  ( dom  F  =  A  ->  dom  F  e.  B ) )
54impcom 419 . . . . 5  |-  ( ( dom  F  =  A  /\  A  e.  B
)  ->  dom  F  e.  B )
6 resfunexg 5737 . . . . 5  |-  ( ( Fun  F  /\  dom  F  e.  B )  -> 
( F  |`  dom  F
)  e.  _V )
75, 6sylan2 460 . . . 4  |-  ( ( Fun  F  /\  ( dom  F  =  A  /\  A  e.  B )
)  ->  ( F  |` 
dom  F )  e. 
_V )
87anassrs 629 . . 3  |-  ( ( ( Fun  F  /\  dom  F  =  A )  /\  A  e.  B
)  ->  ( F  |` 
dom  F )  e. 
_V )
93, 8sylanb 458 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  ( F  |`  dom  F
)  e.  _V )
10 resdm 4993 . . . 4  |-  ( Rel 
F  ->  ( F  |` 
dom  F )  =  F )
1110eleq1d 2349 . . 3  |-  ( Rel 
F  ->  ( ( F  |`  dom  F )  e.  _V  <->  F  e.  _V ) )
1211biimpa 470 . 2  |-  ( ( Rel  F  /\  ( F  |`  dom  F )  e.  _V )  ->  F  e.  _V )
132, 9, 12syl2anc 642 1  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  F  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   _Vcvv 2788   dom cdm 4689    |` cres 4691   Rel wrel 4694   Fun wfun 5249    Fn wfn 5250
This theorem is referenced by:  funex  5743  fex  5749  offval  6085  ofrfval  6086  fndmeng  6937  cfsmolem  7896  axcc2lem  8062  unirnfdomd  8189  prdsbas2  13368  prdsplusgval  13372  prdsmulrval  13374  prdsleval  13376  prdsdsval  13377  prdsvscaval  13378  brssc  13691  sscpwex  13692  ssclem  13696  isssc  13697  rescval2  13705  reschom  13707  rescabs  13710  isfuncd  13739  dprdw  15245  prdsmgp  15393  ptval  17265  elptr  17268  prdstopn  17322  qtoptop  17391  imastopn  17411  ofcfval  23459  vdgrfval  23889  trpredex  24240  wfrlem15  24270  cur1vald  25199  domrancur1clem  25201  domrancur1c  25202  valcurfn1  25204  intopcoaconb  25540  intopcoaconc  25541  dsmmbas2  27203  dsmmelbas  27205  stoweidlem27  27776  stoweidlem59  27808
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263
  Copyright terms: Public domain W3C validator