|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > dff1o3 | Structured version Visualization version GIF version | ||
| Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) | 
| Ref | Expression | 
|---|---|
| dff1o3 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 3anan32 1096 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) | |
| 2 | dff1o2 6852 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
| 3 | df-fo 6566 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
| 4 | 3 | anbi1i 624 | . 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) | 
| 5 | 1, 2, 4 | 3bitr4i 303 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ◡ccnv 5683 ran crn 5685 Fun wfun 6554 Fn wfn 6555 –onto→wfo 6558 –1-1-onto→wf1o 6559 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-ex 1779 df-cleq 2728 df-ss 3967 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 | 
| This theorem is referenced by: f1ofo 6854 resdif 6868 f1opw 7690 f11o 7972 1stconst 8126 2ndconst 8127 curry1 8130 curry2 8133 f1o2ndf1 8148 ssdomg 9041 dif1enlem 9197 dif1enlemOLD 9198 phplem2 9246 php3 9250 phplem4OLD 9258 php3OLD 9262 f1opwfi 9397 cantnfp1lem3 9721 fpwwe2lem5 10676 canthp1lem2 10694 odf1o2 19592 dprdf1o 20053 relogf1o 26609 iseupthf1o 30222 padct 32732 ballotlemfrc 34530 poimirlem1 37629 poimirlem2 37630 poimirlem3 37631 poimirlem4 37632 poimirlem6 37634 poimirlem7 37635 poimirlem9 37637 poimirlem11 37639 poimirlem12 37640 poimirlem13 37641 poimirlem14 37642 poimirlem16 37644 poimirlem17 37645 poimirlem19 37647 poimirlem20 37648 poimirlem23 37651 poimirlem24 37652 poimirlem25 37653 poimirlem29 37657 poimirlem31 37659 ntrneifv2 44098 | 
| Copyright terms: Public domain | W3C validator |