![]() |
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 1122 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) | |
2 | dff1o2 6387 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
3 | df-fo 6133 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | 3 | anbi1i 617 | . 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) |
5 | 1, 2, 4 | 3bitr4i 295 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∧ w3a 1111 = wceq 1656 ◡ccnv 5345 ran crn 5347 Fun wfun 6121 Fn wfn 6122 –onto→wfo 6125 –1-1-onto→wf1o 6126 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-in 3805 df-ss 3812 df-f 6131 df-f1 6132 df-fo 6133 df-f1o 6134 |
This theorem is referenced by: f1ofo 6389 resdif 6402 f1opw 7154 f11o 7395 1stconst 7534 2ndconst 7535 curry1 7538 curry2 7541 f1o2ndf1 7554 ssdomg 8274 phplem4 8417 php3 8421 f1opwfi 8545 cantnfp1lem3 8861 fpwwe2lem6 9779 canthp1lem2 9797 odf1o2 18346 dprdf1o 18792 relogf1o 24719 iseupthf1o 27574 padct 30041 ballotlemfrc 31130 poimirlem1 33953 poimirlem2 33954 poimirlem3 33955 poimirlem4 33956 poimirlem6 33958 poimirlem7 33959 poimirlem9 33961 poimirlem11 33963 poimirlem12 33964 poimirlem13 33965 poimirlem14 33966 poimirlem16 33968 poimirlem17 33969 poimirlem19 33971 poimirlem20 33972 poimirlem23 33975 poimirlem24 33976 poimirlem25 33977 poimirlem29 33981 poimirlem31 33983 ntrneifv2 39217 |
Copyright terms: Public domain | W3C validator |