Theorem dff1o4 6832

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 6829	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1109	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5675	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2774	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 634	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6542	. . . 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 1101   = wceq 1567  ^◡ccnv 5663  dom cdm 5664  ran crn 5665  Fun wfun 6533   Fn wfn 6534  –1-1-onto→wf1o 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1807  df-cleq 2761  df-ss 3930  df-rn 5675  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546

This theorem is referenced by:  f1ocnv  6836  f1oun  6843  f1o00  6859  f1oiOLD  6863  f1osn  6865  f1oprswap  6869  f1ompt  7109  f1ofveu  7407  f1ocnvd  7664  curry1  8101  curry2  8104  mapsnf1o2  8894  omxpenlem  9068  sbthlem9  9085  compssiso  10360  mptfzshft  15831  invf1o  17828  mgmhmf1o  18760  mhmf1o  18856  grpinvf1o  19077  ghmf1o  19320  rnghmf1o  20536  rhmf1o  20575  srngf1o  20931  lmhmf1o  21147  hmeof1o2  23891  axcontlem2  29258  f1o3d  32914  padct  33006  f1od2  33007  cdleme51finvN  41257  fsovf1od  44671  gricushgr  48608  imaf1homlem  49807  idemb  49859