![]() |
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 3079 | . . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | 1 | anim2i 335 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
3 | df-fo 5034 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | df-f 5032 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
5 | 2, 3, 4 | 3imtr4i 200 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1290 ⊆ wss 3000 ran crn 4453 Fn wfn 5023 ⟶wf 5024 –onto→wfo 5026 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-11 1443 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-in 3006 df-ss 3013 df-f 5032 df-fo 5034 |
This theorem is referenced by: fofun 5247 fofn 5248 dffo2 5250 foima 5251 resdif 5288 ffoss 5298 fconstfvm 5529 cocan2 5581 foeqcnvco 5583 fornex 5900 algrflem 6008 algrflemg 6009 tposf2 6047 mapsn 6461 ssdomg 6549 fopwdom 6606 fidcenumlemrks 6716 fidcenumlemr 6718 ctmlemr 6844 ctm 6845 enumctlemm 6846 enumct 6847 fodjuomnilemdc 6860 exmidfodomrlemr 6889 exmidfodomrlemrALT 6890 focdmex 10256 |
Copyright terms: Public domain | W3C validator |