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

Theorem dff1o5 6857
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 6568 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
2 dffo2 6824 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
3 f1f 6804 . . . . 5 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
43biantrurd 532 . . . 4 (𝐹:𝐴1-1𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵)))
52, 4bitr4id 290 . . 3 (𝐹:𝐴1-1𝐵 → (𝐹:𝐴onto𝐵 ↔ ran 𝐹 = 𝐵))
65pm5.32i 574 . 2 ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
71, 6bitri 275 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  ran crn 5686  wf 6557  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568
This theorem is referenced by:  f1orescnv  6863  f1ounsn  7292  domdifsn  9094  sucdom2OLD  9122  sucdom2  9243  ackbij1  10277  ackbij2  10282  fin4en1  10349  om2uzf1oi  13994  s4f1o  14957  fvcosymgeq  19447  indlcim  21860  2lgslem1b  27436  ausgrusgrb  29182  usgrexmpledg  29279  wrdpmtrlast  33113  cdleme50f1o  40548  diaf1oN  41132  aks6d1c2  42131  pwssplit4  43101  cantnf2  43338  meadjiunlem  46480
  Copyright terms: Public domain W3C validator