Theorem dff1o4 6855

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-1onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

Proof of Theorem dff1o4

Step	Hyp	Ref	Expression
1		dff1o2 6852	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
2		3anass 1111	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (𝐹 Fn 𝐴 ∧ (Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)))
3		df-rn 5666	. . . . . 6 ⊢ ran 𝐹 = dom ◡𝐹
4	3	eqeq1i 2768	. . . . 5 ⊢ (ran 𝐹 = 𝐵 ↔ dom ◡𝐹 = 𝐵)
5	4	anbi2i 635	. . . 4 ⊢ ((Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ dom ◡𝐹 = 𝐵))
6		df-fn 6561	. . . 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-1onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ^◡ccnv 5654  dom cdm 5655  ran crn 5656  Fun wfun 6552   Fn wfn 6553  ⟶1-1ontowf1o 6557

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2755  df-ss 3901  df-rn 5666  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565

This theorem is used by:  f1ocnv  6859  f1oun  6866  f1o00  6883  f1oiOLD  6887  f1osn  6889  f1oprswap  6893  f1ompt  7135  f1ofveu  7437  f1ocnvd  7696  f1od2  8135  curry1  8142  curry2  8145  mapsnf1o2  8950  omxpenlem  9125  sbthlem9  9142  compssiso  10479  mptfzshft  15973  invf1o  17973  mgmhmf1o  18918  mhmf1o  19020  grpinvf1o  19248  ghmf1o  19491  rnghmf1o  20712  rhmf1o  20757  srngf1o  21135  lmhmf1o  21351  hmeof1o2  24112  axcontlem2  29573  f1o3d  33292  padct  33381  cdleme51finvN  41805  fsovf1od  45208  gricushgr  49220  imaf1homlem  50428  idemb  50480