![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffo2 | Structured version Visualization version GIF version |
Description: Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.) |
Ref | Expression |
---|---|
dffo2 | ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fof 6805 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | forn 6808 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) | |
3 | 1, 2 | jca 511 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
4 | ffn 6716 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
5 | df-fo 6548 | . . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
6 | 5 | biimpri 227 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵) |
7 | 4, 6 | sylan 579 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵) |
8 | 3, 7 | impbii 208 | 1 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 = wceq 1534 ran crn 5673 Fn wfn 6537 ⟶wf 6538 –onto→wfo 6540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-in 3951 df-ss 3961 df-f 6546 df-fo 6548 |
This theorem is referenced by: focofo 6818 foconst 6820 dff1o5 6842 dffo3 7106 dffo4 7107 exfo 7109 dffo3f 7110 fo1stres 8013 fo2ndres 8014 fo2ndf 8120 cantnf 9708 hsmexlem2 10442 setcepi 18068 odf1o1 19518 efgsfo 19685 pjfo 21636 xrhmeo 24858 grpofo 30296 cnpconn 34776 lnmepi 42431 imasetpreimafvbijlemfo 46668 fargshiftfo 46705 |
Copyright terms: Public domain | W3C validator |