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

Theorem fnex 6119
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 6117. See fnexALT 6749 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 5659 . . 3  |-  ( F  Fn  A  ->  Rel  F )
21adantr 463 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  Rel  F )
3 df-fn 5571 . . 3  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 eleq1a 2485 . . . . . 6  |-  ( A  e.  B  ->  ( dom  F  =  A  ->  dom  F  e.  B ) )
54impcom 428 . . . . 5  |-  ( ( dom  F  =  A  /\  A  e.  B
)  ->  dom  F  e.  B )
6 resfunexg 6117 . . . . 5  |-  ( ( Fun  F  /\  dom  F  e.  B )  -> 
( F  |`  dom  F
)  e.  _V )
75, 6sylan2 472 . . . 4  |-  ( ( Fun  F  /\  ( dom  F  =  A  /\  A  e.  B )
)  ->  ( F  |` 
dom  F )  e. 
_V )
87anassrs 646 . . 3  |-  ( ( ( Fun  F  /\  dom  F  =  A )  /\  A  e.  B
)  ->  ( F  |` 
dom  F )  e. 
_V )
93, 8sylanb 470 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  ( F  |`  dom  F
)  e.  _V )
10 resdm 5134 . . . 4  |-  ( Rel 
F  ->  ( F  |` 
dom  F )  =  F )
1110eleq1d 2471 . . 3  |-  ( Rel 
F  ->  ( ( F  |`  dom  F )  e.  _V  <->  F  e.  _V ) )
1211biimpa 482 . 2  |-  ( ( Rel  F  /\  ( F  |`  dom  F )  e.  _V )  ->  F  e.  _V )
132, 9, 12syl2anc 659 1  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  F  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842   _Vcvv 3058   dom cdm 4822    |` cres 4824   Rel wrel 4827   Fun wfun 5562    Fn wfn 5563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576
This theorem is referenced by:  funex  6120  fex  6125  offval  6527  ofrfval  6528  suppvalfn  6908  suppfnss  6927  fnsuppeq0  6930  wfrlem15  7034  fndmeng  7629  fdmfifsupp  7872  cfsmolem  8681  axcc2lem  8847  unirnfdomd  8973  prdsbas2  15081  prdsplusgval  15085  prdsmulrval  15087  prdsleval  15089  prdsdsval  15090  prdsvscaval  15091  brssc  15425  sscpwex  15426  ssclem  15430  isssc  15431  rescval2  15439  reschom  15441  rescabs  15444  isfuncd  15476  dprdw  17361  dprdwOLD  17368  prdsmgp  17577  dsmmbas2  19064  dsmmelbas  19066  ptval  20361  elptr  20364  prdstopn  20419  qtoptop  20491  imastopn  20511  vdgrfval  25299  suppss3  27983  ofcfval  28531  dya2iocuni  28717  trpredex  30038  stoweidlem27  37158  stoweidlem59  37190
  Copyright terms: Public domain W3C validator