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

Theorem dff1o5 6329
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 6075 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
2 f1f 6283 . . . . 5 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
32biantrurd 528 . . . 4 (𝐹:𝐴1-1𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵)))
4 dffo2 6302 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
53, 4syl6rbbr 281 . . 3 (𝐹:𝐴1-1𝐵 → (𝐹:𝐴onto𝐵 ↔ ran 𝐹 = 𝐵))
65pm5.32i 570 . 2 ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
71, 6bitri 266 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1652  ran crn 5278  wf 6064  1-1wf1 6065  ontowfo 6066  1-1-ontowf1o 6067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3739  df-ss 3746  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075
This theorem is referenced by:  f1orescnv  6335  domdifsn  8250  sucdom2  8363  ackbij1  9313  ackbij2  9318  fin4en1  9384  om2uzf1oi  12960  s4f1o  13949  fvcosymgeq  18114  indlcim  20455  2lgslem1b  25408  ausgrusgrb  26338  usgrexmpledg  26433  cdleme50f1o  36434  diaf1oN  37018  pwssplit4  38268  meadjiunlem  41251
  Copyright terms: Public domain W3C validator