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 ) )