Metamath Proof Explorer


Theorem f1mptrn

Description: Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020)

Ref Expression
Hypotheses f1mptrn.1 φ x A B C
f1mptrn.2 φ y C ∃! x A y = B
Assertion f1mptrn φ Fun x A B -1

Proof

Step Hyp Ref Expression
1 f1mptrn.1 φ x A B C
2 f1mptrn.2 φ y C ∃! x A y = B
3 1 ralrimiva φ x A B C
4 2 ralrimiva φ y C ∃! x A y = B
5 eqid x A B = x A B
6 5 f1ompt x A B : A 1-1 onto C x A B C y C ∃! x A y = B
7 dff1o2 x A B : A 1-1 onto C x A B Fn A Fun x A B -1 ran x A B = C
8 7 simp2bi x A B : A 1-1 onto C Fun x A B -1
9 6 8 sylbir x A B C y C ∃! x A y = B Fun x A B -1
10 3 4 9 syl2anc φ Fun x A B -1