Theorem dff1o4 6825

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 6822	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1111	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5662	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2766	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 635	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6534	. . . 4 ⊢ (◡𝐹 Fn 𝐵 ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
7	5, 6	bitr4i 281	. . 3 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ◡𝐹 Fn 𝐵)
8	7	anbi2i 635	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 300	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ^◡ccnv 5650  dom cdm 5651  ran crn 5652  Fun wfun 6525   Fn wfn 6526  –1-1-onto→wf1o 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2753  df-ss 3916  df-rn 5662  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538

This theorem is used by:  f1ocnv  6829  f1oun  6836  f1o00  6852  f1oiOLD  6856  f1osn  6858  f1oprswap  6862  f1ompt  7103  f1ofveu  7406  f1ocnvd  7664  curry1  8104  curry2  8107  mapsnf1o2  8906  omxpenlem  9081  sbthlem9  9098  compssiso  10433  mptfzshft  15924  invf1o  17924  mgmhmf1o  18869  mhmf1o  18971  grpinvf1o  19199  ghmf1o  19442  rnghmf1o  20662  rhmf1o  20707  srngf1o  21085  lmhmf1o  21301  hmeof1o2  24062  axcontlem2  29525  f1o3d  33202  padct  33292  f1od2  33293  cdleme51finvN  41581  fsovf1od  44975  gricushgr  48959  imaf1homlem  50159  idemb  50211