![]() |
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 3156 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | 1 | anim2i 340 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
3 | df-fo 5137 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | df-f 5135 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3imtr4i 200 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1332 ⊆ wss 3076 ran crn 4548 Fn wfn 5126 ⟶wf 5127 –onto→wfo 5129 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-in 3082 df-ss 3089 df-f 5135 df-fo 5137 |
This theorem is referenced by: fofun 5354 fofn 5355 dffo2 5357 foima 5358 resdif 5397 ffoss 5407 fconstfvm 5646 cocan2 5697 foeqcnvco 5699 fornex 6021 algrflem 6134 algrflemg 6135 tposf2 6173 mapsn 6592 ssdomg 6680 fopwdom 6738 fidcenumlemrks 6849 fidcenumlemr 6851 ctmlemr 7001 ctm 7002 ctssdclemn0 7003 ctssdccl 7004 ctssdc 7006 enumctlemm 7007 enumct 7008 fodjuomnilemdc 7024 exmidfodomrlemr 7075 exmidfodomrlemrALT 7076 suplocexprlemdisj 7552 suplocexprlemub 7555 focdmex 10565 ennnfonelemdc 11948 ennnfonelemg 11952 ennnfonelemp1 11955 ennnfonelemhdmp1 11958 ennnfonelemkh 11961 ennnfonelemhf1o 11962 ennnfonelemex 11963 ennnfonelemhom 11964 ctinfomlemom 11976 ctinf 11979 ctiunctlemudc 11986 ctiunctlemf 11987 omctfn 11992 dvrecap 12885 subctctexmid 13369 pw1nct 13371 |
Copyright terms: Public domain | W3C validator |