Theorem f1stres

Description: Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	f1stres	$$⊢\left({1^{st}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2		vex	$$⊢z\in \mathrm{V}$$
3	1 2	op1sta	$$⊢\bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}=y$$
4	3	eleq1i	$$⊢\bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}\in A\leftrightarrow y\in A$$
5	4	biimpri	$$⊢y\in A\to \bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}\in A$$
6	5	adantr	$$⊢\left(y\in A\wedge z\in B\right)\to \bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}\in A$$
7	6	rgen2	$$⊢\forall y\in A\forall z\in B\bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}\in A$$
8		sneq	$$⊢x=⟨y,z⟩\to \left\{x\right\}=\left\{⟨y,z⟩\right\}$$
9	8	dmeqd	$$⊢x=⟨y,z⟩\to \mathrm{dom}\left\{x\right\}=\mathrm{dom}\left\{⟨y,z⟩\right\}$$
10	9	unieqd	$$⊢x=⟨y,z⟩\to \bigcup \mathrm{dom}\left\{x\right\}=\bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}$$
11	10	eleq1d	$$⊢x=⟨y,z⟩\to \left(\bigcup \mathrm{dom}\left\{x\right\}\in A\leftrightarrow \bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}\in A\right)$$
12	11	ralxp	$$⊢\forall x\in \left(A\times B\right)\bigcup \mathrm{dom}\left\{x\right\}\in A\leftrightarrow \forall y\in A\forall z\in B\bigcup \mathrm{dom}\left\{⟨y,z⟩\right\}\in A$$
13	7 12	mpbir	$$⊢\forall x\in \left(A\times B\right)\bigcup \mathrm{dom}\left\{x\right\}\in A$$
14		df-1st	$$⊢1^{st}=\left(x\in \mathrm{V}⟼\bigcup \mathrm{dom}\left\{x\right\}\right)$$
15	14	reseq1i	$$⊢{1^{st}\upharpoonright }_{\left(A\times B\right)}={\left(x\in \mathrm{V}⟼\bigcup \mathrm{dom}\left\{x\right\}\right)\upharpoonright }_{\left(A\times B\right)}$$
16		ssv	$$⊢A\times B\subseteq \mathrm{V}$$
17		resmpt	$$⊢A\times B\subseteq \mathrm{V}\to {\left(x\in \mathrm{V}⟼\bigcup \mathrm{dom}\left\{x\right\}\right)\upharpoonright }_{\left(A\times B\right)}=\left(x\in \left(A\times B\right)⟼\bigcup \mathrm{dom}\left\{x\right\}\right)$$
18	16 17	ax-mp	$$⊢{\left(x\in \mathrm{V}⟼\bigcup \mathrm{dom}\left\{x\right\}\right)\upharpoonright }_{\left(A\times B\right)}=\left(x\in \left(A\times B\right)⟼\bigcup \mathrm{dom}\left\{x\right\}\right)$$
19	15 18	eqtri	$$⊢{1^{st}\upharpoonright }_{\left(A\times B\right)}=\left(x\in \left(A\times B\right)⟼\bigcup \mathrm{dom}\left\{x\right\}\right)$$
20	19	fmpt	$$⊢\forall x\in \left(A\times B\right)\bigcup \mathrm{dom}\left\{x\right\}\in A\leftrightarrow \left({1^{st}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶A$$
21	13 20	mpbi	$$⊢\left({1^{st}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶A$$