Theorem f1mpt

Description: Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	f1mpt.1	$$⊢F=\left(x\in A⟼C\right)$$
	f1mpt.2	$$⊢x=y\to C=D$$
Assertion	f1mpt	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(\forall x\in AC\in B\wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1mpt.1	$$⊢F=\left(x\in A⟼C\right)$$
2		f1mpt.2	$$⊢x=y\to C=D$$
3		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼C\right)$$
4	1 3	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yF$$
6	4 5	dff13f	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
7	1	fmpt	$$⊢\forall x\in AC\in B\leftrightarrow F:A⟶B$$
8	7	anbi1i	$$⊢\left(\forall x\in AC\in B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
9	2	eleq1d	$$⊢x=y\to \left(C\in B\leftrightarrow D\in B\right)$$
10	9	cbvralvw	$$⊢\forall x\in AC\in B\leftrightarrow \forall y\in AD\in B$$
11		raaanv	$$⊢\forall x\in A\forall y\in A\left(C\in B\wedge D\in B\right)\leftrightarrow \left(\forall x\in AC\in B\wedge \forall y\in AD\in B\right)$$
12	1	fvmpt2	$$⊢\left(x\in A\wedge C\in B\right)\to F\left(x\right)=C$$
13	2 1	fvmptg	$$⊢\left(y\in A\wedge D\in B\right)\to F\left(y\right)=D$$
14	12 13	eqeqan12d	$$⊢\left(\left(x\in A\wedge C\in B\right)\wedge \left(y\in A\wedge D\in B\right)\right)\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow C=D\right)$$
15	14	an4s	$$⊢\left(\left(x\in A\wedge y\in A\right)\wedge \left(C\in B\wedge D\in B\right)\right)\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow C=D\right)$$
16	15	imbi1d	$$⊢\left(\left(x\in A\wedge y\in A\right)\wedge \left(C\in B\wedge D\in B\right)\right)\to \left(\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \left(C=D\to x=y\right)\right)$$
17	16	ex	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left(C\in B\wedge D\in B\right)\to \left(\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \left(C=D\to x=y\right)\right)\right)$$
18	17	ralimdva	$$⊢x\in A\to \left(\forall y\in A\left(C\in B\wedge D\in B\right)\to \forall y\in A\left(\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \left(C=D\to x=y\right)\right)\right)$$
19		ralbi	$$⊢\forall y\in A\left(\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \left(C=D\to x=y\right)\right)\to \left(\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall y\in A\left(C=D\to x=y\right)\right)$$
20	18 19	syl6	$$⊢x\in A\to \left(\forall y\in A\left(C\in B\wedge D\in B\right)\to \left(\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall y\in A\left(C=D\to x=y\right)\right)\right)$$
21	20	ralimia	$$⊢\forall x\in A\forall y\in A\left(C\in B\wedge D\in B\right)\to \forall x\in A\left(\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall y\in A\left(C=D\to x=y\right)\right)$$
22		ralbi	$$⊢\forall x\in A\left(\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall y\in A\left(C=D\to x=y\right)\right)\to \left(\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$
23	21 22	syl	$$⊢\forall x\in A\forall y\in A\left(C\in B\wedge D\in B\right)\to \left(\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$
24	11 23	sylbir	$$⊢\left(\forall x\in AC\in B\wedge \forall y\in AD\in B\right)\to \left(\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$
25	10 24	sylan2b	$$⊢\left(\forall x\in AC\in B\wedge \forall x\in AC\in B\right)\to \left(\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$
26	25	anidms	$$⊢\forall x\in AC\in B\to \left(\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$
27	26	pm5.32i	$$⊢\left(\forall x\in AC\in B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)\leftrightarrow \left(\forall x\in AC\in B\wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$
28	6 8 27	3bitr2i	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(\forall x\in AC\in B\wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)$$