Theorem dff1o2 6867

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 6580	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		df-f1 6578	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3		df-fo 6579	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	2, 3	anbi12i 627	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
5		anass 468	. . . 4 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))))
6		3anan12 1096	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
7	6	anbi1i 623	. . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
8		eqimss 4067	. . . . . . . 8 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
9		df-f 6577	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
10	9	biimpri 228	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → 𝐹:𝐴⟶𝐵)
11	8, 10	sylan2 592	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
12	11	3adant2 1131	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
13	12	pm4.71i 559	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵))
14		ancom 460	. . . . 5 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
15	7, 13, 14	3bitr4ri 304	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
16	5, 15	bitri 275	. . 3 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
17	4, 16	bitri 275	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
18	1, 17	bitri 275	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ⊆ wss 3976  ^◡ccnv 5699  ran crn 5701  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569  –1-1→wf1 6570  –onto→wfo 6571  –1-1-onto→wf1o 6572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580

This theorem is referenced by:  dff1o3  6868  dff1o4  6870  f1orn  6872  tz7.49c  8502  fiint  9394  fiintOLD  9395  symgfixelsi  19477  dfrelog  26625  adj1o  31926  fresf1o  32650  f1mptrn  32654  esumc  34015  sticksstones3  42105  aks6d1c6lem5  42134  cantnf2  43287  ntrneinex  44039  stoweidlem39  45960  uspgrimprop  47757