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

Theorem fnex 6139
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 6137. See fnexALT 6765 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 5684 . . 3  |-  ( F  Fn  A  ->  Rel  F )
21adantr 466 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  Rel  F )
3 df-fn 5596 . . 3  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 eleq1a 2503 . . . . . 6  |-  ( A  e.  B  ->  ( dom  F  =  A  ->  dom  F  e.  B ) )
54impcom 431 . . . . 5  |-  ( ( dom  F  =  A  /\  A  e.  B
)  ->  dom  F  e.  B )
6 resfunexg 6137 . . . . 5  |-  ( ( Fun  F  /\  dom  F  e.  B )  -> 
( F  |`  dom  F
)  e.  _V )
75, 6sylan2 476 . . . 4  |-  ( ( Fun  F  /\  ( dom  F  =  A  /\  A  e.  B )
)  ->  ( F  |` 
dom  F )  e. 
_V )
87anassrs 652 . . 3  |-  ( ( ( Fun  F  /\  dom  F  =  A )  /\  A  e.  B
)  ->  ( F  |` 
dom  F )  e. 
_V )
93, 8sylanb 474 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  ( F  |`  dom  F
)  e.  _V )
10 resdm 5158 . . . 4  |-  ( Rel 
F  ->  ( F  |` 
dom  F )  =  F )
1110eleq1d 2489 . . 3  |-  ( Rel 
F  ->  ( ( F  |`  dom  F )  e.  _V  <->  F  e.  _V ) )
1211biimpa 486 . 2  |-  ( ( Rel  F  /\  ( F  |`  dom  F )  e.  _V )  ->  F  e.  _V )
132, 9, 12syl2anc 665 1  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  F  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1867   _Vcvv 3078   dom cdm 4846    |` cres 4848   Rel wrel 4851   Fun wfun 5587    Fn wfn 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4477  df-mpt 4478  df-id 4761  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601
This theorem is referenced by:  funex  6140  fex  6145  offval  6544  ofrfval  6545  suppvalfn  6924  suppfnss  6943  fnsuppeq0  6946  wfrlem15  7050  fndmeng  7645  fdmfifsupp  7891  cfsmolem  8696  axcc2lem  8862  unirnfdomd  8988  prdsbas2  15345  prdsplusgval  15349  prdsmulrval  15351  prdsleval  15353  prdsdsval  15354  prdsvscaval  15355  brssc  15697  sscpwex  15698  ssclem  15702  isssc  15703  rescval2  15711  reschom  15713  rescabs  15716  isfuncd  15748  dprdw  17620  prdsmgp  17816  dsmmbas2  19277  dsmmelbas  19279  ptval  20562  elptr  20565  prdstopn  20620  qtoptop  20692  imastopn  20712  vdgrfval  25599  suppss3  28297  ofcfval  28908  dya2iocuni  29094  trpredex  30466  stoweidlem27  37674  stoweidlem59  37707  omeiunle  38068
  Copyright terms: Public domain W3C validator