Theorem dff1o4 6811

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 6808	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1105	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5656	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2766	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 632	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6520	. . . 4 ⊢ (◡𝐹 Fn 𝐵 ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
7	5, 6	bitr4i 280	. . 3 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ◡𝐹 Fn 𝐵)
8	7	anbi2i 632	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 299	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559  ^◡ccnv 5644  dom cdm 5645  ran crn 5646  Fun wfun 6511   Fn wfn 6512  –1-1-onto→wf1o 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-ex 1799  df-cleq 2753  df-ss 3921  df-rn 5656  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524

This theorem is referenced by:  f1ocnv  6815  f1oun  6822  f1o00  6838  f1oiOLD  6842  f1osn  6844  f1oprswap  6848  f1ompt  7088  f1ofveu  7386  f1ocnvd  7643  curry1  8078  curry2  8081  mapsnf1o2  8872  omxpenlem  9046  sbthlem9  9063  compssiso  10328  mptfzshft  15788  invf1o  17785  mgmhmf1o  18717  mhmf1o  18813  grpinvf1o  19034  ghmf1o  19271  rnghmf1o  20480  rhmf1o  20519  srngf1o  20877  lmhmf1o  21093  hmeof1o2  23803  axcontlem2  29112  f1o3d  32778  padct  32870  f1od2  32871  cdleme51finvN  41144  fsovf1od  44556  gricushgr  48503  imaf1homlem  49692  idemb  49744