Theorem dff1o4 6831

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
dff1o4	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

Proof of Theorem dff1o4

Step	Hyp	Ref	Expression
1		dff1o2 6828	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1111	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5674	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2768	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 634	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6541	. . . 4 ⊢ (◡𝐹 Fn 𝐵 ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
7	5, 6	bitr4i 281	. . 3 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ◡𝐹 Fn 𝐵)
8	7	anbi2i 634	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 300	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570  ^◡ccnv 5662  dom cdm 5663  ran crn 5664  Fun wfun 6532   Fn wfn 6533  –1-1-onto→wf1o 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-cleq 2755  df-ss 3923  df-rn 5674  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is referenced by:  f1ocnv  6835  f1oun  6842  f1o00  6858  f1oiOLD  6862  f1osn  6864  f1oprswap  6868  f1ompt  7108  f1ofveu  7406  f1ocnvd  7663  curry1  8100  curry2  8103  mapsnf1o2  8893  omxpenlem  9067  sbthlem9  9084  compssiso  10359  mptfzshft  15831  invf1o  17827  mgmhmf1o  18759  mhmf1o  18855  grpinvf1o  19076  ghmf1o  19319  rnghmf1o  20535  rhmf1o  20574  srngf1o  20932  lmhmf1o  21148  hmeof1o2  23901  axcontlem2  29293  f1o3d  32949  padct  33041  f1od2  33042  cdleme51finvN  41308  fsovf1od  44722  gricushgr  48659  imaf1homlem  49862  idemb  49914