Theorem dff1o2 6615

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 6357	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		df-f1 6355	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3		df-fo 6356	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	2, 3	anbi12i 628	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
5		anass 471	. . . 4 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))))
6		3anan12 1092	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
7	6	anbi1i 625	. . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
8		eqimss 4023	. . . . . . . 8 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
9		df-f 6354	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
10	9	biimpri 230	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → 𝐹:𝐴⟶𝐵)
11	8, 10	sylan2 594	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
12	11	3adant2 1127	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
13	12	pm4.71i 562	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵))
14		ancom 463	. . . . 5 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
15	7, 13, 14	3bitr4ri 306	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
16	5, 15	bitri 277	. . 3 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
17	4, 16	bitri 277	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
18	1, 17	bitri 277	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ⊆ wss 3936  ^◡ccnv 5549  ran crn 5551  Fun wfun 6344   Fn wfn 6345  ⟶wf 6346  –1-1→wf1 6347  –onto→wfo 6348  –1-1-onto→wf1o 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357

This theorem is referenced by:  dff1o3  6616  dff1o4  6618  f1orn  6620  tz7.49c  8076  fiint  8789  symgfixelsi  18557  dfrelog  25143  adj1o  29665  fresf1o  30370  f1mptrn  30374  esumc  31305  ntrneinex  40420  stoweidlem39  42317