Theorem dff1o4 6819

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 6816	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1109	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5663	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2770	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 634	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6528	. . . 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 1563  ^◡ccnv 5651  dom cdm 5652  ran crn 5653  Fun wfun 6519   Fn wfn 6520  –1-1-onto→wf1o 6524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1803  df-cleq 2757  df-ss 3924  df-rn 5663  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532

This theorem is referenced by:  f1ocnv  6823  f1oun  6830  f1o00  6846  f1oiOLD  6850  f1osn  6852  f1oprswap  6856  f1ompt  7096  f1ofveu  7394  f1ocnvd  7651  curry1  8087  curry2  8090  mapsnf1o2  8880  omxpenlem  9054  sbthlem9  9071  compssiso  10346  mptfzshft  15819  invf1o  17816  mgmhmf1o  18748  mhmf1o  18844  grpinvf1o  19066  ghmf1o  19309  rnghmf1o  20525  rhmf1o  20564  srngf1o  20920  lmhmf1o  21136  hmeof1o2  23881  axcontlem2  29224  f1o3d  32883  padct  32975  f1od2  32976  cdleme51finvN  41192  fsovf1od  44604  gricushgr  48537  imaf1homlem  49736  idemb  49788