Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > foima | Structured version Visualization version GIF version |
Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.) |
Ref | Expression |
---|---|
foima | ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imadmrn 5979 | . 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹 | |
2 | fof 6688 | . . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
3 | 2 | fdmd 6611 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴) |
4 | 3 | imaeq2d 5969 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴)) |
5 | forn 6691 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) | |
6 | 1, 4, 5 | 3eqtr3a 2802 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 dom cdm 5589 ran crn 5590 “ cima 5592 –onto→wfo 6431 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-xp 5595 df-cnv 5597 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-fn 6436 df-f 6437 df-fo 6439 |
This theorem is referenced by: foimacnv 6733 domunfican 9087 fiint 9091 fodomfi 9092 cantnflt2 9431 cantnfp1lem3 9438 enfin1ai 10140 symgfixelsi 19043 dprdf1o 19635 lmimlbs 21043 cncmp 22543 cmpfi 22559 cnconn 22573 qtopval2 22847 elfm3 23101 rnelfm 23104 fmfnfmlem2 23106 fmfnfm 23109 eupthvdres 28599 pjordi 30535 qtophaus 31786 poimirlem1 35778 poimirlem2 35779 poimirlem3 35780 poimirlem4 35781 poimirlem5 35782 poimirlem6 35783 poimirlem7 35784 poimirlem9 35786 poimirlem10 35787 poimirlem11 35788 poimirlem12 35789 poimirlem14 35791 poimirlem16 35793 poimirlem17 35794 poimirlem19 35796 poimirlem20 35797 poimirlem22 35799 poimirlem23 35800 poimirlem24 35801 poimirlem25 35802 poimirlem29 35806 poimirlem31 35808 ovoliunnfl 35819 voliunnfl 35821 volsupnfl 35822 ismtybndlem 35964 kelac1 40888 gicabl 40924 |
Copyright terms: Public domain | W3C validator |