This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1mptrn

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

Ref Expression
Hypotheses f1mptrn.1 
|- ( ( ph /\ x e. A ) -> B e. C )
f1mptrn.2 
|- ( ( ph /\ y e. C ) -> E! x e. A y = B )
Assertion f1mptrn 
|- ( ph -> Fun `' ( x e. A |-> B ) )

Proof

Step Hyp Ref Expression
1 f1mptrn.1 
 |-  ( ( ph /\ x e. A ) -> B e. C )
2 f1mptrn.2 
 |-  ( ( ph /\ y e. C ) -> E! x e. A y = B )
3 1 ralrimiva 
 |-  ( ph -> A. x e. A B e. C )
4 2 ralrimiva 
 |-  ( ph -> A. y e. C E! x e. A y = B )
5 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
6 5 f1ompt 
 |-  ( ( x e. A |-> B ) : A -1-1-onto-> C <-> ( A. x e. A B e. C /\ A. y e. C E! x e. A y = B ) )
7 dff1o2 
 |-  ( ( x e. A |-> B ) : A -1-1-onto-> C <-> ( ( x e. A |-> B ) Fn A /\ Fun `' ( x e. A |-> B ) /\ ran ( x e. A |-> B ) = C ) )
8 7 simp2bi 
 |-  ( ( x e. A |-> B ) : A -1-1-onto-> C -> Fun `' ( x e. A |-> B ) )
9 6 8 sylbir 
 |-  ( ( A. x e. A B e. C /\ A. y e. C E! x e. A y = B ) -> Fun `' ( x e. A |-> B ) )
10 3 4 9 syl2anc 
 |-  ( ph -> Fun `' ( x e. A |-> B ) )