![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1ofun | Structured version Visualization version GIF version |
Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1ofun | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ofn 6392 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
2 | fnfun 6233 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6129 Fn wfn 6130 –1-1-onto→wf1o 6134 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 199 df-an 387 df-fn 6138 df-f 6139 df-f1 6140 df-f1o 6142 |
This theorem is referenced by: f1orel 6394 f1oresrab 6659 fveqf1o 6829 isofrlem 6862 isofr 6864 isose 6865 f1opw 7166 xpcomco 8338 f1opwfi 8558 inlresf 9073 inrresf 9075 djuun 9085 isercolllem2 14804 isercoll 14806 unbenlem 16016 gsumpropd2lem 17659 symgfixf1 18240 tgqtop 21924 hmeontr 21981 reghmph 22005 nrmhmph 22006 tgpconncompeqg 22323 cnheiborlem 23161 dfrelog 24749 dvloglem 24831 logf1o2 24833 axcontlem9 26321 axcontlem10 26322 padct 30063 madjusmdetlem2 30492 tpr2rico 30556 ballotlemrv 31180 reprpmtf1o 31306 hgt750lemg 31334 subfacp1lem2a 31761 subfacp1lem2b 31762 subfacp1lem5 31765 ismtyres 34231 diaclN 37204 dia1elN 37208 diaintclN 37212 docaclN 37278 dibintclN 37321 sge0f1o 41523 f1oresf1o 42331 f1oresf1o2 42332 |
Copyright terms: Public domain | W3C validator |