Theorem dff1o2 6841

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 6554	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		df-f1 6552	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3		df-fo 6553	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	2, 3	anbi12i 626	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
5		anass 467	. . . 4 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))))
6		3anan12 1093	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
7	6	anbi1i 622	. . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
8		eqimss 4036	. . . . . . . 8 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
9		df-f 6551	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
10	9	biimpri 227	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → 𝐹:𝐴⟶𝐵)
11	8, 10	sylan2 591	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
12	11	3adant2 1128	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
13	12	pm4.71i 558	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵))
14		ancom 459	. . . . 5 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
15	7, 13, 14	3bitr4ri 303	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
16	5, 15	bitri 274	. . 3 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
17	4, 16	bitri 274	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
18	1, 17	bitri 274	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ⊆ wss 3945  ^◡ccnv 5676  ran crn 5678  Fun wfun 6541   Fn wfn 6542  ⟶wf 6543  –1-1→wf1 6544  –onto→wfo 6545  –1-1-onto→wf1o 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-ex 1774  df-cleq 2717  df-ss 3962  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554

This theorem is referenced by:  dff1o3  6842  dff1o4  6844  f1orn  6846  tz7.49c  8465  fiint  9348  symgfixelsi  19394  dfrelog  26529  adj1o  31760  fresf1o  32473  f1mptrn  32477  esumc  33740  sticksstones3  41689  aks6d1c6lem5  41718  cantnf2  42819  ntrneinex  43572  stoweidlem39  45490  uspgrimprop  47283