Theorem dff1o4 6647

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 6644	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1097	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5547	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2741	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 626	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6361	. . . 4 ⊢ (◡𝐹 Fn 𝐵 ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
7	5, 6	bitr4i 281	. . 3 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ◡𝐹 Fn 𝐵)
8	7	anbi2i 626	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9	1, 2, 8	3bitri 300	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543  ^◡ccnv 5535  dom cdm 5536  ran crn 5537  Fun wfun 6352   Fn wfn 6353  –1-1-onto→wf1o 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-rn 5547  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365

This theorem is referenced by:  f1ocnv  6651  f1oun  6658  f1o00  6673  f1oi  6676  f1osn  6678  f1oprswap  6682  f1ompt  6906  f1ofveu  7186  f1ocnvd  7434  curry1  7850  curry2  7853  mapsnf1o2  8553  omxpenlem  8724  sbthlem9  8742  compssiso  9953  mptfzshft  15305  invf1o  17228  mhmf1o  18182  grpinvf1o  18387  ghmf1o  18606  rhmf1o  19706  srngf1o  19844  lmhmf1o  20037  hmeof1o2  22614  axcontlem2  27010  f1o3d  30635  padct  30728  f1od2  30730  cdleme51finvN  38256  fsovf1od  41242  isomushgr  44894  mgmhmf1o  44957  rnghmf1o  45077