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

Theorem fnex 6118
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 6740 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 5670 . . 3  |-  ( F  Fn  A  ->  Rel  F )
21adantr 465 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  Rel  F )
3 df-fn 5582 . . 3  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
4 eleq1a 2543 . . . . . 6  |-  ( A  e.  B  ->  ( dom  F  =  A  ->  dom  F  e.  B ) )
54impcom 430 . . . . 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 474 . . . 4  |-  ( ( Fun  F  /\  ( dom  F  =  A  /\  A  e.  B )
)  ->  ( F  |` 
dom  F )  e. 
_V )
87anassrs 648 . . 3  |-  ( ( ( Fun  F  /\  dom  F  =  A )  /\  A  e.  B
)  ->  ( F  |` 
dom  F )  e. 
_V )
93, 8sylanb 472 . 2  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  ( F  |`  dom  F
)  e.  _V )
10 resdm 5306 . . . 4  |-  ( Rel 
F  ->  ( F  |` 
dom  F )  =  F )
1110eleq1d 2529 . . 3  |-  ( Rel 
F  ->  ( ( F  |`  dom  F )  e.  _V  <->  F  e.  _V ) )
1211biimpa 484 . 2  |-  ( ( Rel  F  /\  ( F  |`  dom  F )  e.  _V )  ->  F  e.  _V )
132, 9, 12syl2anc 661 1  |-  ( ( F  Fn  A  /\  A  e.  B )  ->  F  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   _Vcvv 3106   dom cdm 4992    |` cres 4994   Rel wrel 4997   Fun wfun 5573    Fn wfn 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587
This theorem is referenced by:  funex  6119  fex  6124  offval  6522  ofrfval  6523  suppvalfn  6898  suppfnss  6915  fnsuppeq0  6918  fndmeng  7582  fdmfifsupp  7828  cfsmolem  8639  axcc2lem  8805  unirnfdomd  8931  prdsbas2  14713  prdsplusgval  14717  prdsmulrval  14719  prdsleval  14721  prdsdsval  14722  prdsvscaval  14723  brssc  15033  sscpwex  15034  ssclem  15038  isssc  15039  rescval2  15047  reschom  15049  rescabs  15052  isfuncd  15081  dprdw  16827  dprdwOLD  16833  prdsmgp  17036  dsmmbas2  18528  dsmmelbas  18530  ptval  19799  elptr  19802  prdstopn  19857  qtoptop  19929  imastopn  19949  vdgrfval  24557  suppss3  27208  ofcfval  27723  dya2iocuni  27880  trpredex  28883  wfrlem15  28920  stoweidlem27  31282  stoweidlem59  31314
  Copyright terms: Public domain W3C validator