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

Theorem dff1o5 6623
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 6361 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
2 f1f 6574 . . . . 5 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
32biantrurd 533 . . . 4 (𝐹:𝐴1-1𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵)))
4 dffo2 6593 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
53, 4syl6rbbr 291 . . 3 (𝐹:𝐴1-1𝐵 → (𝐹:𝐴onto𝐵 ↔ ran 𝐹 = 𝐵))
65pm5.32i 575 . 2 ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
71, 6bitri 276 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1530  ran crn 5555  wf 6350  1-1wf1 6351  ontowfo 6352  1-1-ontowf1o 6353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-in 3947  df-ss 3956  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361
This theorem is referenced by:  f1orescnv  6629  domdifsn  8594  sucdom2  8708  ackbij1  9654  ackbij2  9659  fin4en1  9725  om2uzf1oi  13316  s4f1o  14275  fvcosymgeq  18493  indlcim  20919  2lgslem1b  25901  ausgrusgrb  26883  usgrexmpledg  26977  cdleme50f1o  37568  diaf1oN  38152  pwssplit4  39573  meadjiunlem  42632
  Copyright terms: Public domain W3C validator