Theorem dff1o4 6771

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 6768	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1094	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5627	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2736	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 623	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6484	. . . 4 ⊢ (◡𝐹 Fn 𝐵 ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
7	5, 6	bitr4i 278	. . 3 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ◡𝐹 Fn 𝐵)
8	7	anbi2i 623	. 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 1086   = wceq 1541  ^◡ccnv 5615  dom cdm 5616  ran crn 5617  Fun wfun 6475   Fn wfn 6476  –1-1-onto→wf1o 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2723  df-ss 3919  df-rn 5627  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  f1ocnv  6775  f1oun  6782  f1o00  6798  f1oi  6801  f1osn  6803  f1oprswap  6807  f1ompt  7044  f1ofveu  7340  f1ocnvd  7597  curry1  8034  curry2  8037  mapsnf1o2  8818  omxpenlem  8991  sbthlem9  9008  compssiso  10262  mptfzshft  15682  invf1o  17673  mgmhmf1o  18605  mhmf1o  18701  grpinvf1o  18919  ghmf1o  19158  rnghmf1o  20368  rhmf1o  20406  srngf1o  20761  lmhmf1o  20978  hmeof1o2  23676  axcontlem2  28941  f1o3d  32603  padct  32696  f1od2  32697  cdleme51finvN  40594  fsovf1od  44048  gricushgr  47947  imaf1homlem  49138  idemb  49190