Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmpt2d Structured version   Visualization version   GIF version

Theorem fmpt2d 6882
 Description: Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.)
Hypotheses
Ref Expression
fmpt2d.2 ((𝜑𝑥𝐴) → 𝐵𝑉)
fmpt2d.1 (𝜑𝐹 = (𝑥𝐴𝐵))
fmpt2d.3 ((𝜑𝑦𝐴) → (𝐹𝑦) ∈ 𝐶)
Assertion
Ref Expression
fmpt2d (𝜑𝐹:𝐴𝐶)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐶   𝑦,𝐹   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥)   𝐹(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem fmpt2d
StepHypRef Expression
1 fmpt2d.2 . . . . 5 ((𝜑𝑥𝐴) → 𝐵𝑉)
21ralrimiva 3186 . . . 4 (𝜑 → ∀𝑥𝐴 𝐵𝑉)
3 eqid 2825 . . . . 5 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 6484 . . . 4 (∀𝑥𝐴 𝐵𝑉 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . 3 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 fmpt2d.1 . . . 4 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 6442 . . 3 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 258 . 2 (𝜑𝐹 Fn 𝐴)
9 fmpt2d.3 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) ∈ 𝐶)
109ralrimiva 3186 . 2 (𝜑 → ∀𝑦𝐴 (𝐹𝑦) ∈ 𝐶)
11 ffnfv 6877 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) ∈ 𝐶))
128, 10, 11sylanbrc 583 1 (𝜑𝐹:𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1530   ∈ wcel 2107  ∀wral 3142   ↦ cmpt 5142   Fn wfn 6346  ⟶wf 6347  ‘cfv 6351 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-fv 6359 This theorem is referenced by:  cantnff  9129  limsupgre  14831  idaf  17315  curfcl  17474  mat2pmatf  21254  m2cpmf  21268  pm2mpf  21324  clsf  21574  kgenf  22067  lgamf  25535  vmaf  25612  lgsdchr  25847  mirf  26362  suppovss  30343  omsf  31442  erdszelem6  32329  cdleme50f  37547  dochfN  38361  binomcxplemdvsum  40554
 Copyright terms: Public domain W3C validator