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

Theorem dff1o4 6357
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 6354 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
2 3anass 1109 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)))
3 df-rn 5322 . . . . . 6 ran 𝐹 = dom 𝐹
43eqeq1i 2811 . . . . 5 (ran 𝐹 = 𝐵 ↔ dom 𝐹 = 𝐵)
54anbi2i 611 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
6 df-fn 6100 . . . 4 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
75, 6bitr4i 269 . . 3 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ 𝐹 Fn 𝐵)
87anbi2i 611 . 2 ((𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
91, 2, 83bitri 288 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  w3a 1100   = wceq 1637  ccnv 5310  dom cdm 5311  ran crn 5312  Fun wfun 6091   Fn wfn 6092  1-1-ontowf1o 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783  df-rn 5322  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104
This theorem is referenced by:  f1ocnv  6361  f1oun  6368  f1o00  6383  f1oi  6386  f1osn  6388  f1oprswap  6392  f1ompt  6599  f1ofveu  6865  f1ocnvd  7110  curry1  7499  curry2  7502  mapsnf1o2  8138  omxpenlem  8296  sbthlem9  8313  compssiso  9477  mptfzshft  14728  fsumrev  14729  fprodrev  14924  invf1o  16629  mhmf1o  17546  grpinvf1o  17686  ghmf1o  17888  rhmf1o  18932  srngf1o  19054  lmhmf1o  19249  hmeof1o2  21777  axcontlem2  26058  f1o3d  29757  padct  29823  f1od2  29825  cdleme51finvN  36334  fsovf1od  38807  mgmhmf1o  42352  rnghmf1o  42468
  Copyright terms: Public domain W3C validator