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

Theorem dff1o2 6790
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
dff1o2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dff1o2
StepHypRef Expression
1 df-f1o 6504 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
2 df-f1 6502 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
3 df-fo 6503 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
42, 3anbi12i 628 . . 3 ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ ((𝐹:𝐴𝐵 ∧ Fun 𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
5 anass 470 . . . 4 (((𝐹:𝐴𝐵 ∧ Fun 𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹:𝐴𝐵 ∧ (Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))))
6 3anan12 1097 . . . . . 6 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
76anbi1i 625 . . . . 5 (((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴𝐵) ↔ ((Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴𝐵))
8 eqimss 4001 . . . . . . . 8 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
9 df-f 6501 . . . . . . . . 9 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
109biimpri 227 . . . . . . . 8 ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → 𝐹:𝐴𝐵)
118, 10sylan2 594 . . . . . . 7 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴𝐵)
12113adant2 1132 . . . . . 6 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴𝐵)
1312pm4.71i 561 . . . . 5 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴𝐵))
14 ancom 462 . . . . 5 ((𝐹:𝐴𝐵 ∧ (Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ ((Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴𝐵))
157, 13, 143bitr4ri 304 . . . 4 ((𝐹:𝐴𝐵 ∧ (Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
165, 15bitri 275 . . 3 (((𝐹:𝐴𝐵 ∧ Fun 𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
174, 16bitri 275 . 2 ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
181, 17bitri 275 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  w3a 1088   = wceq 1542  wss 3911  ccnv 5633  ran crn 5635  Fun wfun 6491   Fn wfn 6492  wf 6493  1-1wf1 6494  ontowfo 6495  1-1-ontowf1o 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  dff1o3  6791  dff1o4  6793  f1orn  6795  tz7.49c  8393  fiint  9269  symgfixelsi  19218  dfrelog  25924  adj1o  30839  fresf1o  31548  f1mptrn  31552  esumc  32653  sticksstones3  40559  cantnf2  41662  ntrneinex  42356  stoweidlem39  44287
  Copyright terms: Public domain W3C validator