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

Theorem dff1o4 6452
 Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
dff1o4 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))

Proof of Theorem dff1o4
StepHypRef Expression
1 dff1o2 6449 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
2 3anass 1076 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)))
3 df-rn 5418 . . . . . 6 ran 𝐹 = dom 𝐹
43eqeq1i 2784 . . . . 5 (ran 𝐹 = 𝐵 ↔ dom 𝐹 = 𝐵)
54anbi2i 613 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
6 df-fn 6191 . . . 4 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
75, 6bitr4i 270 . . 3 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ 𝐹 Fn 𝐵)
87anbi2i 613 . 2 ((𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
91, 2, 83bitri 289 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507  ◡ccnv 5406  dom cdm 5407  ran crn 5408  Fun wfun 6182   Fn wfn 6183  –1-1-onto→wf1o 6187 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-in 3837  df-ss 3844  df-rn 5418  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195 This theorem is referenced by:  f1ocnv  6456  f1oun  6463  f1o00  6478  f1oi  6481  f1osn  6483  f1oprswap  6487  f1ompt  6698  f1ofveu  6971  f1ocnvd  7214  curry1  7607  curry2  7610  mapsnf1o2  8256  omxpenlem  8414  sbthlem9  8431  compssiso  9594  mptfzshft  14993  fprodrev  15191  invf1o  16897  mhmf1o  17813  grpinvf1o  17956  ghmf1o  18159  rhmf1o  19207  srngf1o  19347  lmhmf1o  19540  hmeof1o2  22075  axcontlem2  26454  f1o3d  30136  padct  30207  f1od2  30209  cdleme51finvN  37134  fsovf1od  39722  isomushgr  43357  mgmhmf1o  43420  rnghmf1o  43536
 Copyright terms: Public domain W3C validator