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 1043 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) | |
2 | dff1o2 6055 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
3 | df-fo 5810 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | 3 | anbi1i 727 | . 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) |
5 | 1, 2, 4 | 3bitr4i 291 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ◡ccnv 5037 ran crn 5039 Fun wfun 5798 Fn wfn 5799 –onto→wfo 5802 –1-1-onto→wf1o 5803 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 |
This theorem is referenced by: f1ofo 6057 resdif 6070 f1opw 6787 f11o 7021 1stconst 7152 2ndconst 7153 curry1 7156 curry2 7159 f1o2ndf1 7172 ssdomg 7887 phplem4 8027 php3 8031 f1opwfi 8153 cantnfp1lem3 8460 fpwwe2lem6 9336 canthp1lem2 9354 odf1o2 17811 dprdf1o 18254 relogf1o 24117 padct 28885 ballotlemfrc 29915 poimirlem1 32580 poimirlem2 32581 poimirlem3 32582 poimirlem4 32583 poimirlem6 32585 poimirlem7 32586 poimirlem9 32588 poimirlem11 32590 poimirlem12 32591 poimirlem13 32592 poimirlem14 32593 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 poimirlem23 32602 poimirlem24 32603 poimirlem25 32604 poimirlem29 32608 poimirlem31 32610 ntrneifv2 37398 iseupthf1o 41369 |
Copyright terms: Public domain | W3C validator |