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

Theorem dff1o4 6102
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 6099 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
2 3anass 1040 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)))
3 df-rn 5085 . . . . . 6 ran 𝐹 = dom 𝐹
43eqeq1i 2626 . . . . 5 (ran 𝐹 = 𝐵 ↔ dom 𝐹 = 𝐵)
54anbi2i 729 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
6 df-fn 5850 . . . 4 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
75, 6bitr4i 267 . . 3 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ 𝐹 Fn 𝐵)
87anbi2i 729 . 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 384  w3a 1036   = wceq 1480  ccnv 5073  dom cdm 5074  ran crn 5075  Fun wfun 5841   Fn wfn 5842  1-1-ontowf1o 5846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569  df-rn 5085  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854
This theorem is referenced by:  f1ocnv  6106  f1oun  6113  f1o00  6128  f1oi  6131  f1osn  6133  f1oprswap  6137  f1ompt  6338  f1ofveu  6599  f1ocnvd  6837  curry1  7214  curry2  7217  mapsnf1o2  7849  omxpenlem  8005  sbthlem9  8022  compssiso  9140  mptfzshft  14438  fsumrev  14439  fprodrev  14632  invf1o  16350  mhmf1o  17266  grpinvf1o  17406  ghmf1o  17611  rhmf1o  18653  srngf1o  18775  lmhmf1o  18965  hmeof1o2  21476  axcontlem2  25745  f1o3d  29272  padct  29337  f1od2  29339  cdleme51finvN  35321  fsovf1od  37789  mgmhmf1o  41072  rnghmf1o  41188
  Copyright terms: Public domain W3C validator