Theorem dff1o4 6790

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 6787	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1095	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5643	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2742	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 624	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6503	. . . 4 ⊢ (◡𝐹 Fn 𝐵 ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
7	5, 6	bitr4i 278	. . 3 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ◡𝐹 Fn 𝐵)
8	7	anbi2i 624	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 297	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ^◡ccnv 5631  dom cdm 5632  ran crn 5633  Fun wfun 6494   Fn wfn 6495  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2729  df-ss 3920  df-rn 5643  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1ocnv  6794  f1oun  6801  f1o00  6817  f1oiOLD  6821  f1osn  6823  f1oprswap  6827  f1ompt  7065  f1ofveu  7362  f1ocnvd  7619  curry1  8056  curry2  8059  mapsnf1o2  8844  omxpenlem  9018  sbthlem9  9035  compssiso  10296  mptfzshft  15713  invf1o  17705  mgmhmf1o  18637  mhmf1o  18733  grpinvf1o  18951  ghmf1o  19189  rnghmf1o  20400  rhmf1o  20438  srngf1o  20793  lmhmf1o  21010  hmeof1o2  23719  axcontlem2  29050  f1o3d  32715  padct  32807  f1od2  32808  cdleme51finvN  40926  fsovf1od  44366  gricushgr  48271  imaf1homlem  49460  idemb  49512