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

Theorem f1o2d 7682
Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
Hypotheses
Ref Expression
f1od.1 𝐹 = (𝑥𝐴𝐶)
f1o2d.2 ((𝜑𝑥𝐴) → 𝐶𝐵)
f1o2d.3 ((𝜑𝑦𝐵) → 𝐷𝐴)
f1o2d.4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))
Assertion
Ref Expression
f1o2d (𝜑𝐹:𝐴1-1-onto𝐵)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑦,𝐶   𝑥,𝐷   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem f1o2d
StepHypRef Expression
1 f1od.1 . . 3 𝐹 = (𝑥𝐴𝐶)
2 f1o2d.2 . . 3 ((𝜑𝑥𝐴) → 𝐶𝐵)
3 f1o2d.3 . . 3 ((𝜑𝑦𝐵) → 𝐷𝐴)
4 f1o2d.4 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))
51, 2, 3, 4f1ocnv2d 7681 . 2 (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐹 = (𝑦𝐵𝐷)))
65simpld 493 1 (𝜑𝐹:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099  cmpt 5238  ccnv 5683  1-1-ontowf1o 6555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5306  ax-nul 5313  ax-pr 5435
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5156  df-opab 5218  df-mpt 5239  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563
This theorem is referenced by:  f1opw2  7683  en3d  9022  f1opwfi  9402  mapfien  9453  djulf1o  9957  djurf1o  9958  fin23lem22  10372  negf1o  11696  incexclem  15842  dvdsflip  16321  hashgcdlem  16792  grplmulf1o  19009  grpraddf1o  19010  conjghm  19245  gapm  19302  sylow2a  19619  lsmhash  19705  psrbagconf1o  21936  psrbagconf1oOLD  21937  psdmul  22162  hmeoimaf1o  23768  itg1mulc  25728  resinf1o  26566  eff1olem  26578  sqff1o  27213  dvdsppwf1o  27217  dvdsflf1o  27218  fcobij  32638  mgcf1o  32875  subfacp1lem3  35012  subfacp1lem5  35014  metakunt15  41907  metakunt16  41908  f1o2d2  41959  frlmsnic  42210
  Copyright terms: Public domain W3C validator