Theorem dff1o5 6308

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

Assertion

Ref	Expression
dff1o5	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dff1o5

Step	Hyp	Ref	Expression
1		df-f1o 6056	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		f1f 6262	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	biantrurd 530	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)))
4		dffo2 6281	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
5	3, 4	syl6rbbr 279	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴–onto→𝐵 ↔ ran 𝐹 = 𝐵))
6	5	pm5.32i 672	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))
7	1, 6	bitri 264	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1632  ran crn 5267  ⟶wf 6045  –1-1→wf1 6046  –onto→wfo 6047  –1-1-onto→wf1o 6048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056

This theorem is referenced by:  f1orescnv  6314  domdifsn  8210  sucdom2  8323  ackbij1  9272  ackbij2  9277  fin4en1  9343  om2uzf1oi  12966  s4f1o  13883  fvcosymgeq  18069  indlcim  20401  2lgslem1b  25337  ausgrusgrb  26280  usgrexmpledg  26374  cdleme50f1o  36354  diaf1oN  36939  pwssplit4  38179  meadjiunlem  41203