Metamath Proof Explorer


Theorem f1mpt

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

Ref Expression
Hypotheses f1mpt.1 F=xAC
f1mpt.2 x=yC=D
Assertion f1mpt F:A1-1BxACBxAyAC=Dx=y

Proof

Step Hyp Ref Expression
1 f1mpt.1 F=xAC
2 f1mpt.2 x=yC=D
3 nfmpt1 _xxAC
4 1 3 nfcxfr _xF
5 nfcv _yF
6 4 5 dff13f F:A1-1BF:ABxAyAFx=Fyx=y
7 1 fmpt xACBF:AB
8 7 anbi1i xACBxAyAFx=Fyx=yF:ABxAyAFx=Fyx=y
9 2 eleq1d x=yCBDB
10 9 cbvralvw xACByADB
11 raaanv xAyACBDBxACByADB
12 1 fvmpt2 xACBFx=C
13 2 1 fvmptg yADBFy=D
14 12 13 eqeqan12d xACByADBFx=FyC=D
15 14 an4s xAyACBDBFx=FyC=D
16 15 imbi1d xAyACBDBFx=Fyx=yC=Dx=y
17 16 ex xAyACBDBFx=Fyx=yC=Dx=y
18 17 ralimdva xAyACBDByAFx=Fyx=yC=Dx=y
19 ralbi yAFx=Fyx=yC=Dx=yyAFx=Fyx=yyAC=Dx=y
20 18 19 syl6 xAyACBDByAFx=Fyx=yyAC=Dx=y
21 20 ralimia xAyACBDBxAyAFx=Fyx=yyAC=Dx=y
22 ralbi xAyAFx=Fyx=yyAC=Dx=yxAyAFx=Fyx=yxAyAC=Dx=y
23 21 22 syl xAyACBDBxAyAFx=Fyx=yxAyAC=Dx=y
24 11 23 sylbir xACByADBxAyAFx=Fyx=yxAyAC=Dx=y
25 10 24 sylan2b xACBxACBxAyAFx=Fyx=yxAyAC=Dx=y
26 25 anidms xACBxAyAFx=Fyx=yxAyAC=Dx=y
27 26 pm5.32i xACBxAyAFx=Fyx=yxACBxAyAC=Dx=y
28 6 8 27 3bitr2i F:A1-1BxACBxAyAC=Dx=y