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

Theorem dff1o4 6598
 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 6595 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
2 3anass 1092 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)))
3 df-rn 5530 . . . . . 6 ran 𝐹 = dom 𝐹
43eqeq1i 2803 . . . . 5 (ran 𝐹 = 𝐵 ↔ dom 𝐹 = 𝐵)
54anbi2i 625 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
6 df-fn 6327 . . . 4 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
75, 6bitr4i 281 . . 3 ((Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ 𝐹 Fn 𝐵)
87anbi2i 625 . 2 ((𝐹 Fn 𝐴 ∧ (Fun 𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
91, 2, 83bitri 300 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ◡ccnv 5518  dom cdm 5519  ran crn 5520  Fun wfun 6318   Fn wfn 6319  –1-1-onto→wf1o 6323 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-rn 5530  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331 This theorem is referenced by:  f1ocnv  6602  f1oun  6609  f1o00  6624  f1oi  6627  f1osn  6629  f1oprswap  6633  f1ompt  6852  f1ofveu  7130  f1ocnvd  7376  curry1  7782  curry2  7785  mapsnf1o2  8441  omxpenlem  8601  sbthlem9  8619  compssiso  9785  mptfzshft  15125  fprodrev  15323  invf1o  17031  mhmf1o  17958  grpinvf1o  18161  ghmf1o  18380  rhmf1o  19480  srngf1o  19618  lmhmf1o  19811  hmeof1o2  22368  axcontlem2  26759  f1o3d  30386  padct  30481  f1od2  30483  cdleme51finvN  37852  fsovf1od  40715  isomushgr  44342  mgmhmf1o  44405  rnghmf1o  44525
 Copyright terms: Public domain W3C validator