Metamath Proof Explorer

Theorem elimampt

Description: Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022)

Ref Expression
Hypotheses elimampt.f ${⊢}{F}=\left({x}\in {A}⟼{B}\right)$
elimampt.c ${⊢}{\phi }\to {C}\in {W}$
elimampt.d ${⊢}{\phi }\to {D}\subseteq {A}$
Assertion elimampt ${⊢}{\phi }\to \left({C}\in {F}\left[{D}\right]↔\exists {x}\in {D}\phantom{\rule{.4em}{0ex}}{C}={B}\right)$

Proof

Step Hyp Ref Expression
1 elimampt.f ${⊢}{F}=\left({x}\in {A}⟼{B}\right)$
2 elimampt.c ${⊢}{\phi }\to {C}\in {W}$
3 elimampt.d ${⊢}{\phi }\to {D}\subseteq {A}$
4 df-ima ${⊢}{F}\left[{D}\right]=\mathrm{ran}\left({{F}↾}_{{D}}\right)$
5 4 eleq2i ${⊢}{C}\in {F}\left[{D}\right]↔{C}\in \mathrm{ran}\left({{F}↾}_{{D}}\right)$
6 1 reseq1i ${⊢}{{F}↾}_{{D}}={\left({x}\in {A}⟼{B}\right)↾}_{{D}}$
7 resmpt ${⊢}{D}\subseteq {A}\to {\left({x}\in {A}⟼{B}\right)↾}_{{D}}=\left({x}\in {D}⟼{B}\right)$
8 6 7 syl5eq ${⊢}{D}\subseteq {A}\to {{F}↾}_{{D}}=\left({x}\in {D}⟼{B}\right)$
9 8 rneqd ${⊢}{D}\subseteq {A}\to \mathrm{ran}\left({{F}↾}_{{D}}\right)=\mathrm{ran}\left({x}\in {D}⟼{B}\right)$
10 9 eleq2d ${⊢}{D}\subseteq {A}\to \left({C}\in \mathrm{ran}\left({{F}↾}_{{D}}\right)↔{C}\in \mathrm{ran}\left({x}\in {D}⟼{B}\right)\right)$
11 3 10 syl ${⊢}{\phi }\to \left({C}\in \mathrm{ran}\left({{F}↾}_{{D}}\right)↔{C}\in \mathrm{ran}\left({x}\in {D}⟼{B}\right)\right)$
12 eqid ${⊢}\left({x}\in {D}⟼{B}\right)=\left({x}\in {D}⟼{B}\right)$
13 12 elrnmpt ${⊢}{C}\in {W}\to \left({C}\in \mathrm{ran}\left({x}\in {D}⟼{B}\right)↔\exists {x}\in {D}\phantom{\rule{.4em}{0ex}}{C}={B}\right)$
14 2 13 syl ${⊢}{\phi }\to \left({C}\in \mathrm{ran}\left({x}\in {D}⟼{B}\right)↔\exists {x}\in {D}\phantom{\rule{.4em}{0ex}}{C}={B}\right)$
15 11 14 bitrd ${⊢}{\phi }\to \left({C}\in \mathrm{ran}\left({{F}↾}_{{D}}\right)↔\exists {x}\in {D}\phantom{\rule{.4em}{0ex}}{C}={B}\right)$
16 5 15 syl5bb ${⊢}{\phi }\to \left({C}\in {F}\left[{D}\right]↔\exists {x}\in {D}\phantom{\rule{.4em}{0ex}}{C}={B}\right)$