Metamath Proof Explorer

Theorem f1elima

Description: Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion f1elima ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\wedge {Y}\subseteq {A}\right)\to \left({F}\left({X}\right)\in {F}\left[{Y}\right]↔{X}\in {Y}\right)$

Proof

Step Hyp Ref Expression
1 f1fn ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to {F}Fn{A}$
2 fvelimab ${⊢}\left({F}Fn{A}\wedge {Y}\subseteq {A}\right)\to \left({F}\left({X}\right)\in {F}\left[{Y}\right]↔\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)\right)$
3 1 2 sylan ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {Y}\subseteq {A}\right)\to \left({F}\left({X}\right)\in {F}\left[{Y}\right]↔\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)\right)$
4 3 3adant2 ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\wedge {Y}\subseteq {A}\right)\to \left({F}\left({X}\right)\in {F}\left[{Y}\right]↔\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)\right)$
5 ssel ${⊢}{Y}\subseteq {A}\to \left({z}\in {Y}\to {z}\in {A}\right)$
6 5 impac ${⊢}\left({Y}\subseteq {A}\wedge {z}\in {Y}\right)\to \left({z}\in {A}\wedge {z}\in {Y}\right)$
7 f1fveq ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \left({z}\in {A}\wedge {X}\in {A}\right)\right)\to \left({F}\left({z}\right)={F}\left({X}\right)↔{z}={X}\right)$
8 7 ancom2s ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \left({X}\in {A}\wedge {z}\in {A}\right)\right)\to \left({F}\left({z}\right)={F}\left({X}\right)↔{z}={X}\right)$
9 8 biimpd ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \left({X}\in {A}\wedge {z}\in {A}\right)\right)\to \left({F}\left({z}\right)={F}\left({X}\right)\to {z}={X}\right)$
10 9 anassrs ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\right)\wedge {z}\in {A}\right)\to \left({F}\left({z}\right)={F}\left({X}\right)\to {z}={X}\right)$
11 eleq1 ${⊢}{z}={X}\to \left({z}\in {Y}↔{X}\in {Y}\right)$
12 11 biimpcd ${⊢}{z}\in {Y}\to \left({z}={X}\to {X}\in {Y}\right)$
13 10 12 sylan9 ${⊢}\left(\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\right)\wedge {z}\in {A}\right)\wedge {z}\in {Y}\right)\to \left({F}\left({z}\right)={F}\left({X}\right)\to {X}\in {Y}\right)$
14 13 anasss ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\right)\wedge \left({z}\in {A}\wedge {z}\in {Y}\right)\right)\to \left({F}\left({z}\right)={F}\left({X}\right)\to {X}\in {Y}\right)$
15 6 14 sylan2 ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\right)\wedge \left({Y}\subseteq {A}\wedge {z}\in {Y}\right)\right)\to \left({F}\left({z}\right)={F}\left({X}\right)\to {X}\in {Y}\right)$
16 15 anassrs ${⊢}\left(\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\right)\wedge {Y}\subseteq {A}\right)\wedge {z}\in {Y}\right)\to \left({F}\left({z}\right)={F}\left({X}\right)\to {X}\in {Y}\right)$
17 16 rexlimdva ${⊢}\left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\right)\wedge {Y}\subseteq {A}\right)\to \left(\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)\to {X}\in {Y}\right)$
18 17 3impa ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\wedge {Y}\subseteq {A}\right)\to \left(\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)\to {X}\in {Y}\right)$
19 eqid ${⊢}{F}\left({X}\right)={F}\left({X}\right)$
20 fveqeq2 ${⊢}{z}={X}\to \left({F}\left({z}\right)={F}\left({X}\right)↔{F}\left({X}\right)={F}\left({X}\right)\right)$
21 20 rspcev ${⊢}\left({X}\in {Y}\wedge {F}\left({X}\right)={F}\left({X}\right)\right)\to \exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)$
22 19 21 mpan2 ${⊢}{X}\in {Y}\to \exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)$
23 18 22 impbid1 ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\wedge {Y}\subseteq {A}\right)\to \left(\exists {z}\in {Y}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={F}\left({X}\right)↔{X}\in {Y}\right)$
24 4 23 bitrd ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {X}\in {A}\wedge {Y}\subseteq {A}\right)\to \left({F}\left({X}\right)\in {F}\left[{Y}\right]↔{X}\in {Y}\right)$