f1elima

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

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

Proof

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

Metamath Proof Explorer

Theorem f1elima

Proof