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 5941 | . 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹 | |
2 | fof 6592 | . . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
3 | 2 | fdmd 6525 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴) |
4 | 3 | imaeq2d 5931 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴)) |
5 | forn 6595 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) | |
6 | 1, 4, 5 | 3eqtr3a 2882 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 dom cdm 5557 ran crn 5558 “ cima 5560 –onto→wfo 6355 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pr 5332 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-br 5069 df-opab 5131 df-xp 5563 df-cnv 5565 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-fn 6360 df-f 6361 df-fo 6363 |
This theorem is referenced by: foimacnv 6634 domunfican 8793 fiint 8797 fodomfi 8799 cantnflt2 9138 cantnfp1lem3 9145 enfin1ai 9808 symgfixelsi 18565 dprdf1o 19156 lmimlbs 20982 cncmp 22002 cmpfi 22018 cnconn 22032 qtopval2 22306 elfm3 22560 rnelfm 22563 fmfnfmlem2 22565 fmfnfm 22568 eupthvdres 28016 pjordi 29952 qtophaus 31102 poimirlem1 34895 poimirlem2 34896 poimirlem3 34897 poimirlem4 34898 poimirlem5 34899 poimirlem6 34900 poimirlem7 34901 poimirlem9 34903 poimirlem10 34904 poimirlem11 34905 poimirlem12 34906 poimirlem14 34908 poimirlem16 34910 poimirlem17 34911 poimirlem19 34913 poimirlem20 34914 poimirlem22 34916 poimirlem23 34917 poimirlem24 34918 poimirlem25 34919 poimirlem29 34923 poimirlem31 34925 ovoliunnfl 34936 voliunnfl 34938 volsupnfl 34939 ismtybndlem 35086 kelac1 39670 gicabl 39706 |
Copyright terms: Public domain | W3C validator |