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

Theorem dff1o5 6611
 Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
dff1o5 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dff1o5
StepHypRef Expression
1 df-f1o 6342 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
2 dffo2 6580 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
3 f1f 6560 . . . . 5 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
43biantrurd 536 . . . 4 (𝐹:𝐴1-1𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵)))
52, 4bitr4id 293 . . 3 (𝐹:𝐴1-1𝐵 → (𝐹:𝐴onto𝐵 ↔ ran 𝐹 = 𝐵))
65pm5.32i 578 . 2 ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
71, 6bitri 278 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ran crn 5525  ⟶wf 6331  –1-1→wf1 6332  –onto→wfo 6333  –1-1-onto→wf1o 6334 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 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342 This theorem is referenced by:  f1orescnv  6617  domdifsn  8621  sucdom2  8648  ackbij1  9698  ackbij2  9703  fin4en1  9769  om2uzf1oi  13370  s4f1o  14327  fvcosymgeq  18624  indlcim  20605  2lgslem1b  26075  ausgrusgrb  27057  usgrexmpledg  27151  cdleme50f1o  38122  diaf1oN  38706  pwssplit4  40406  meadjiunlem  43470
 Copyright terms: Public domain W3C validator