mptpreima

Description: The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015)

		Ref	Expression
	Hypothesis	dmmpt.1	$⊢ F = (x \in A ⟼ B)$
	Assertion	mptpreima	$⊢ F^{-1} [C] = \{x \in A \| B \in C\}$

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	$⊢ F = (x \in A ⟼ B)$
2		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
3	1 2	eqtri	$⊢ F = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
4	3	cnveqi	$⊢ F^{-1} = {\{⟨x, y⟩ \| (x \in A \land y = B)\}}^{-1}$
5		cnvopab	$⊢ {\{⟨x, y⟩ \| (x \in A \land y = B)\}}^{-1} = \{⟨y, x⟩ \| (x \in A \land y = B)\}$
6	4 5	eqtri	$⊢ F^{-1} = \{⟨y, x⟩ \| (x \in A \land y = B)\}$
7	6	imaeq1i	$⊢ F^{-1} [C] = \{⟨y, x⟩ \| (x \in A \land y = B)\} [C]$
8		df-ima	$⊢ \{⟨y, x⟩ \| (x \in A \land y = B)\} [C] = ran ({\{⟨y, x⟩ \| (x \in A \land y = B)\} ↾}_{C})$
9		resopab	$⊢ {\{⟨y, x⟩ \| (x \in A \land y = B)\} ↾}_{C} = \{⟨y, x⟩ \| (y \in C \land (x \in A \land y = B))\}$
10	9	rneqi	$⊢ ran ({\{⟨y, x⟩ \| (x \in A \land y = B)\} ↾}_{C}) = ran \{⟨y, x⟩ \| (y \in C \land (x \in A \land y = B))\}$
11		ancom	$⊢ (y \in C \land (x \in A \land y = B)) \leftrightarrow ((x \in A \land y = B) \land y \in C)$
12		anass	$⊢ ((x \in A \land y = B) \land y \in C) \leftrightarrow (x \in A \land (y = B \land y \in C))$
13	11 12	bitri	$⊢ (y \in C \land (x \in A \land y = B)) \leftrightarrow (x \in A \land (y = B \land y \in C))$
14	13	exbii	$⊢ \exists y (y \in C \land (x \in A \land y = B)) \leftrightarrow \exists y (x \in A \land (y = B \land y \in C))$
15		19.42v	$⊢ \exists y (x \in A \land (y = B \land y \in C)) \leftrightarrow (x \in A \land \exists y (y = B \land y \in C))$
16		dfclel	$⊢ B \in C \leftrightarrow \exists y (y = B \land y \in C)$
17	16	bicomi	$⊢ \exists y (y = B \land y \in C) \leftrightarrow B \in C$
18	17	anbi2i	$⊢ (x \in A \land \exists y (y = B \land y \in C)) \leftrightarrow (x \in A \land B \in C)$
19	15 18	bitri	$⊢ \exists y (x \in A \land (y = B \land y \in C)) \leftrightarrow (x \in A \land B \in C)$
20	14 19	bitri	$⊢ \exists y (y \in C \land (x \in A \land y = B)) \leftrightarrow (x \in A \land B \in C)$
21	20	abbii	$⊢ \{x \| \exists y (y \in C \land (x \in A \land y = B))\} = \{x \| (x \in A \land B \in C)\}$
22		rnopab	$⊢ ran \{⟨y, x⟩ \| (y \in C \land (x \in A \land y = B))\} = \{x \| \exists y (y \in C \land (x \in A \land y = B))\}$
23		df-rab	$⊢ \{x \in A \| B \in C\} = \{x \| (x \in A \land B \in C)\}$
24	21 22 23	3eqtr4i	$⊢ ran \{⟨y, x⟩ \| (y \in C \land (x \in A \land y = B))\} = \{x \in A \| B \in C\}$
25	10 24	eqtri	$⊢ ran ({\{⟨y, x⟩ \| (x \in A \land y = B)\} ↾}_{C}) = \{x \in A \| B \in C\}$
26	8 25	eqtri	$⊢ \{⟨y, x⟩ \| (x \in A \land y = B)\} [C] = \{x \in A \| B \in C\}$
27	7 26	eqtri	$⊢ F^{-1} [C] = \{x \in A \| B \in C\}$

Metamath Proof Explorer

Theorem mptpreima

Proof