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

Theorem dff1o4 6828
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 6825 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
2 3anass 1095 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)))
3 df-rn 5680 . . . . . 6 ran 𝐹 = dom 𝐹
43eqeq1i 2736 . . . . 5 (ran 𝐹 = 𝐵 ↔ dom 𝐹 = 𝐵)
54anbi2i 623 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
6 df-fn 6535 . . . 4 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
75, 6bitr4i 277 . . 3 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ 𝐹 Fn 𝐵)
87anbi2i 623 . 2 ((𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
91, 2, 83bitri 296 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3a 1087   = wceq 1541  ccnv 5668  dom cdm 5669  ran crn 5670  Fun wfun 6526   Fn wfn 6527  1-1-ontowf1o 6531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-rn 5680  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539
This theorem is referenced by:  f1ocnv  6832  f1oun  6839  f1o00  6855  f1oi  6858  f1osn  6860  f1oprswap  6864  f1ompt  7095  f1ofveu  7387  f1ocnvd  7640  curry1  8072  curry2  8075  mapsnf1o2  8871  omxpenlem  9056  sbthlem9  9074  compssiso  10351  mptfzshft  15706  invf1o  17698  mhmf1o  18658  grpinvf1o  18867  ghmf1o  19088  rhmf1o  20219  srngf1o  20411  lmhmf1o  20606  hmeof1o2  23196  axcontlem2  28088  f1o3d  31719  padct  31815  f1od2  31817  cdleme51finvN  39232  fsovf1od  42538  isomushgr  46266  mgmhmf1o  46329  rnghmf1o  46449
  Copyright terms: Public domain W3C validator