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

Theorem dff1o2 6853
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 6568 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
2 df-f1 6566 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
3 df-fo 6567 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
42, 3anbi12i 628 . . 3 ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ ((𝐹:𝐴𝐵 ∧ Fun 𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
5 anass 468 . . . 4 (((𝐹:𝐴𝐵 ∧ Fun 𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹:𝐴𝐵 ∧ (Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))))
6 3anan12 1096 . . . . . 6 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
76anbi1i 624 . . . . 5 (((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴𝐵) ↔ ((Fun 𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴𝐵))
8 eqimss 4042 . . . . . . . 8 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
9 df-f 6565 . . . . . . . . 9 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
109biimpri 228 . . . . . . . 8 ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → 𝐹:𝐴𝐵)
118, 10sylan2 593 . . . . . . 7 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴𝐵)
12113adant2 1132 . . . . . 6 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴𝐵)
1312pm4.71i 559 . . . . 5 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴𝐵))
14 ancom 460 . . . . 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 206  wa 395  w3a 1087   = wceq 1540  wss 3951  ccnv 5684  ran crn 5686  Fun wfun 6555   Fn wfn 6556  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-3an 1089  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:  dff1o3  6854  dff1o4  6856  f1orn  6858  tz7.49c  8486  fiint  9366  fiintOLD  9367  symgfixelsi  19453  dfrelog  26607  adj1o  31913  fresf1o  32641  f1mptrn  32645  esumc  34052  sticksstones3  42149  aks6d1c6lem5  42178  cantnf2  43338  ntrneinex  44090  stoweidlem39  46054  uspgrimprop  47873
  Copyright terms: Public domain W3C validator