Metamath Proof Explorer


Theorem fmpt

Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis fmpt.1 F = x A C
Assertion fmpt x A C B F : A B

Proof

Step Hyp Ref Expression
1 fmpt.1 F = x A C
2 1 fnmpt x A C B F Fn A
3 1 rnmpt ran F = y | x A y = C
4 r19.29 x A C B x A y = C x A C B y = C
5 eleq1 y = C y B C B
6 5 biimparc C B y = C y B
7 6 rexlimivw x A C B y = C y B
8 4 7 syl x A C B x A y = C y B
9 8 ex x A C B x A y = C y B
10 9 abssdv x A C B y | x A y = C B
11 3 10 eqsstrid x A C B ran F B
12 df-f F : A B F Fn A ran F B
13 2 11 12 sylanbrc x A C B F : A B
14 fimacnv F : A B F -1 B = A
15 1 mptpreima F -1 B = x A | C B
16 14 15 eqtr3di F : A B A = x A | C B
17 rabid2 A = x A | C B x A C B
18 16 17 sylib F : A B x A C B
19 13 18 impbii x A C B F : A B