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

Theorem dff1o4 6306
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 6303 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
2 3anass 1081 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)))
3 df-rn 5277 . . . . . 6 ran 𝐹 = dom 𝐹
43eqeq1i 2765 . . . . 5 (ran 𝐹 = 𝐵 ↔ dom 𝐹 = 𝐵)
54anbi2i 732 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
6 df-fn 6052 . . . 4 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
75, 6bitr4i 267 . . 3 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ 𝐹 Fn 𝐵)
87anbi2i 732 . 2 ((𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
91, 2, 83bitri 286 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1072   = wceq 1632  ccnv 5265  dom cdm 5266  ran crn 5267  Fun wfun 6043   Fn wfn 6044  1-1-ontowf1o 6048
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729  df-rn 5277  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056
This theorem is referenced by:  f1ocnv  6310  f1oun  6317  f1o00  6332  f1oi  6335  f1osn  6337  f1oprswap  6341  f1ompt  6545  f1ofveu  6808  f1ocnvd  7049  curry1  7437  curry2  7440  mapsnf1o2  8071  omxpenlem  8226  sbthlem9  8243  compssiso  9388  mptfzshft  14709  fsumrev  14710  fprodrev  14906  invf1o  16630  mhmf1o  17546  grpinvf1o  17686  ghmf1o  17891  rhmf1o  18934  srngf1o  19056  lmhmf1o  19248  hmeof1o2  21768  axcontlem2  26044  f1o3d  29740  padct  29806  f1od2  29808  cdleme51finvN  36346  fsovf1od  38812  mgmhmf1o  42297  rnghmf1o  42413
  Copyright terms: Public domain W3C validator