fipreima

Description: Given a finite subset A of the range of a function, there exists a finite subset of the domain whose image is A . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 22-Feb-2015)

		Ref	Expression
	Assertion	fipreima	$⊢ (F Fn B \land A \subseteq ran F \land A \in Fin) \to \exists c \in (𝒫 B \cap Fin) F [c] = A$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (F Fn B \land A \subseteq ran F \land A \in Fin) \to A \in Fin$
2		dfss3	$⊢ A \subseteq ran F \leftrightarrow \forall x \in A x \in ran F$
3		fvelrnb	$⊢ F Fn B \to (x \in ran F \leftrightarrow \exists y \in B F (y) = x)$
4	3	ralbidv	$⊢ F Fn B \to (\forall x \in A x \in ran F \leftrightarrow \forall x \in A \exists y \in B F (y) = x)$
5	2 4	bitrid	$⊢ F Fn B \to (A \subseteq ran F \leftrightarrow \forall x \in A \exists y \in B F (y) = x)$
6	5	biimpa	$⊢ (F Fn B \land A \subseteq ran F) \to \forall x \in A \exists y \in B F (y) = x$
7	6	3adant3	$⊢ (F Fn B \land A \subseteq ran F \land A \in Fin) \to \forall x \in A \exists y \in B F (y) = x$
8		fveqeq2	$⊢ y = f (x) \to (F (y) = x \leftrightarrow F (f (x)) = x)$
9	8	ac6sfi	$⊢ (A \in Fin \land \forall x \in A \exists y \in B F (y) = x) \to \exists f (f : A ⟶ B \land \forall x \in A F (f (x)) = x)$
10	1 7 9	syl2anc	$⊢ (F Fn B \land A \subseteq ran F \land A \in Fin) \to \exists f (f : A ⟶ B \land \forall x \in A F (f (x)) = x)$
11		fimass	$⊢ f : A ⟶ B \to f [A] \subseteq B$
12		vex	$⊢ f \in V$
13	12	imaex	$⊢ f [A] \in V$
14	13	elpw	$⊢ f [A] \in 𝒫 B \leftrightarrow f [A] \subseteq B$
15	11 14	sylibr	$⊢ f : A ⟶ B \to f [A] \in 𝒫 B$
16	15	ad2antrl	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to f [A] \in 𝒫 B$
17		ffun	$⊢ f : A ⟶ B \to Fun f$
18	17	ad2antrl	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to Fun f$
19		simpl3	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to A \in Fin$
20		imafi	$⊢ (Fun f \land A \in Fin) \to f [A] \in Fin$
21	18 19 20	syl2anc	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to f [A] \in Fin$
22	16 21	elind	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to f [A] \in (𝒫 B \cap Fin)$
23		fvco3	$⊢ (f : A ⟶ B \land x \in A) \to (F \circ f) (x) = F (f (x))$
24		fvresi	$⊢ x \in A \to ({I ↾}_{A}) (x) = x$
25	24	adantl	$⊢ (f : A ⟶ B \land x \in A) \to ({I ↾}_{A}) (x) = x$
26	23 25	eqeq12d	$⊢ (f : A ⟶ B \land x \in A) \to ((F \circ f) (x) = ({I ↾}_{A}) (x) \leftrightarrow F (f (x)) = x)$
27	26	ralbidva	$⊢ f : A ⟶ B \to (\forall x \in A (F \circ f) (x) = ({I ↾}_{A}) (x) \leftrightarrow \forall x \in A F (f (x)) = x)$
28	27	biimprd	$⊢ f : A ⟶ B \to (\forall x \in A F (f (x)) = x \to \forall x \in A (F \circ f) (x) = ({I ↾}_{A}) (x))$
29	28	adantl	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land f : A ⟶ B) \to (\forall x \in A F (f (x)) = x \to \forall x \in A (F \circ f) (x) = ({I ↾}_{A}) (x))$
30	29	impr	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to \forall x \in A (F \circ f) (x) = ({I ↾}_{A}) (x)$
31		simpl1	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to F Fn B$
32		ffn	$⊢ f : A ⟶ B \to f Fn A$
33	32	ad2antrl	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to f Fn A$
34		frn	$⊢ f : A ⟶ B \to ran f \subseteq B$
35	34	ad2antrl	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to ran f \subseteq B$
36		fnco	$⊢ (F Fn B \land f Fn A \land ran f \subseteq B) \to (F \circ f) Fn A$
37	31 33 35 36	syl3anc	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to (F \circ f) Fn A$
38		fnresi	$⊢ ({I ↾}_{A}) Fn A$
39		eqfnfv	$⊢ ((F \circ f) Fn A \land ({I ↾}_{A}) Fn A) \to (F \circ f = {I ↾}_{A} \leftrightarrow \forall x \in A (F \circ f) (x) = ({I ↾}_{A}) (x))$
40	37 38 39	sylancl	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to (F \circ f = {I ↾}_{A} \leftrightarrow \forall x \in A (F \circ f) (x) = ({I ↾}_{A}) (x))$
41	30 40	mpbird	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to F \circ f = {I ↾}_{A}$
42	41	imaeq1d	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to (F \circ f) [A] = ({I ↾}_{A}) [A]$
43		imaco	$⊢ (F \circ f) [A] = F [f [A]]$
44		ssid	$⊢ A \subseteq A$
45		resiima	$⊢ A \subseteq A \to ({I ↾}_{A}) [A] = A$
46	44 45	ax-mp	$⊢ ({I ↾}_{A}) [A] = A$
47	42 43 46	3eqtr3g	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to F [f [A]] = A$
48		imaeq2	$⊢ c = f [A] \to F [c] = F [f [A]]$
49	48	eqeq1d	$⊢ c = f [A] \to (F [c] = A \leftrightarrow F [f [A]] = A)$
50	49	rspcev	$⊢ (f [A] \in (𝒫 B \cap Fin) \land F [f [A]] = A) \to \exists c \in (𝒫 B \cap Fin) F [c] = A$
51	22 47 50	syl2anc	$⊢ ((F Fn B \land A \subseteq ran F \land A \in Fin) \land (f : A ⟶ B \land \forall x \in A F (f (x)) = x)) \to \exists c \in (𝒫 B \cap Fin) F [c] = A$
52	10 51	exlimddv	$⊢ (F Fn B \land A \subseteq ran F \land A \in Fin) \to \exists c \in (𝒫 B \cap Fin) F [c] = A$

Metamath Proof Explorer

Theorem fipreima

Proof