![]() |
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 6854 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
3 | df-fo 6569 | . . 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 1537 ◡ccnv 5688 ran crn 5690 Fun wfun 6557 Fn wfn 6558 –onto→wfo 6561 –1-1-onto→wf1o 6562 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-ex 1777 df-cleq 2727 df-ss 3980 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 |
This theorem is referenced by: f1ofo 6856 resdif 6870 f1opw 7689 f11o 7970 1stconst 8124 2ndconst 8125 curry1 8128 curry2 8131 f1o2ndf1 8146 ssdomg 9039 dif1enlem 9195 dif1enlemOLD 9196 phplem2 9243 php3 9247 phplem4OLD 9255 php3OLD 9259 f1opwfi 9394 cantnfp1lem3 9718 fpwwe2lem5 10673 canthp1lem2 10691 odf1o2 19606 dprdf1o 20067 relogf1o 26623 iseupthf1o 30231 padct 32737 ballotlemfrc 34508 poimirlem1 37608 poimirlem2 37609 poimirlem3 37610 poimirlem4 37611 poimirlem6 37613 poimirlem7 37614 poimirlem9 37616 poimirlem11 37618 poimirlem12 37619 poimirlem13 37620 poimirlem14 37621 poimirlem16 37623 poimirlem17 37624 poimirlem19 37626 poimirlem20 37627 poimirlem23 37630 poimirlem24 37631 poimirlem25 37632 poimirlem29 37636 poimirlem31 37638 ntrneifv2 44070 |
Copyright terms: Public domain | W3C validator |