Theorem dff1o2 6816

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 6532	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		df-f1 6530	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3		df-fo 6531	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	2, 3	anbi12i 639	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
5		anass 473	. . . 4 ⊢ (((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ↔ (𝐹:𝐴⟶𝐵 ∧ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))))
6		3anan12 1110	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ (Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)))
7	6	anbi1i 635	. . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) ∧ 𝐹:𝐴⟶𝐵))
8		eqimss 3997	. . . . . . . 8 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
9		df-f 6529	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
10	9	biimpri 231	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → 𝐹:𝐴⟶𝐵)
11	8, 10	sylan2 604	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
12	11	3adant2 1147	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵)
13	12	pm4.71i 568	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ∧ 𝐹:𝐴⟶𝐵))
14		ancom 465	. . . . 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 𝐹 = 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ⊆ wss 3907  ^◡ccnv 5651  ran crn 5653  Fun wfun 6519   Fn wfn 6520  ⟶wf 6521  –1-1→wf1 6522  –onto→wfo 6523  –1-1-onto→wf1o 6524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1803  df-cleq 2757  df-ss 3924  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532

This theorem is referenced by:  dff1o3  6817  dff1o4  6819  f1orn  6821  f1oi  6849  tz7.49c  8421  fiint  9274  symgfixelsi  19496  dfrelog  26688  adj1o  32155  fresf1o  32888  f1mptrn  32892  esumc  34358  sticksstones3  42777  aks6d1c6lem5  42806  cantnf2  43914  ntrneinex  44665  stoweidlem39  46611