Theorem dff1o2 6827

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
dff1o2	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dff1o2

Step	Hyp	Ref	Expression
1		df-f1o 6544	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		df-f1 6542	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3		df-fo 6543	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	2, 3	anbi12i 640	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
5		anass 474	. . . 4 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))))
6		3anan12 1112	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
7	6	anbi1i 636	. . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
8		eqimss 3992	. . . . . . . 8 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
9		df-f 6541	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
10	9	biimpri 231	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → 𝐹:𝐴⟶𝐵)
11	8, 10	sylan2 605	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
12	11	3adant2 1149	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
13	12	pm4.71i 569	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵))
14		ancom 466	. . . . 5 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
15	7, 13, 14	3bitr4ri 307	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
16	5, 15	bitri 278	. . 3 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
17	4, 16	bitri 278	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
18	1, 17	bitri 278	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ⊆ wss 3902  ^◡ccnv 5658  ran crn 5660  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  –1-1→wf1 6534  –onto→wfo 6535  –1-1-onto→wf1o 6536

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2754  df-ss 3919  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is used by:  dff1o3  6828  dff1o4  6830  f1orn  6832  f1oi  6860  tz7.49c  8439  fiint  9300  symgfixelsi  19568  dfrelog  26810  adj1o  32383  fresf1o  33112  f1mptrn  33116  esumc  34569  sticksstones3  43022  aks6d1c6lem5  43051  cantnf2  44174  ntrneinex  44925  stoweidlem39  46875