![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fof | GIF version |
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
fof | ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 3221 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | 1 | anim2i 342 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
3 | df-fo 5234 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | df-f 5232 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3imtr4i 201 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1363 ⊆ wss 3141 ran crn 4639 Fn wfn 5223 ⟶wf 5224 –onto→wfo 5226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-in 3147 df-ss 3154 df-f 5232 df-fo 5234 |
This theorem is referenced by: fofun 5451 fofn 5452 dffo2 5454 foima 5455 resdif 5495 ffoss 5505 fconstfvm 5747 cocan2 5802 foeqcnvco 5804 focdmex 6130 algrflem 6244 algrflemg 6245 tposf2 6283 mapsn 6704 ssdomg 6792 fopwdom 6850 fidcenumlemrks 6966 fidcenumlemr 6968 ctmlemr 7121 ctm 7122 ctssdclemn0 7123 ctssdccl 7124 ctssdc 7126 enumctlemm 7127 enumct 7128 fodjuomnilemdc 7156 exmidfodomrlemr 7215 exmidfodomrlemrALT 7216 suplocexprlemdisj 7733 suplocexprlemub 7736 ennnfonelemdc 12414 ennnfonelemg 12418 ennnfonelemp1 12421 ennnfonelemhdmp1 12424 ennnfonelemkh 12427 ennnfonelemhf1o 12428 ennnfonelemex 12429 ennnfonelemhom 12430 ctinfomlemom 12442 ctinf 12445 ctiunctlemudc 12452 ctiunctlemf 12453 omctfn 12458 imasival 12745 imasbas 12746 imasplusg 12747 imasmulr 12748 imasaddfnlemg 12753 imasaddvallemg 12754 imasaddflemg 12755 imasgrp2 13013 mhmid 13018 mhmmnd 13019 mhmfmhm 13020 ghmgrp 13021 imasring 13369 dvrecap 14530 subctctexmid 15104 pw1nct 15106 |
Copyright terms: Public domain | W3C validator |