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 = ( x e. A |-> C )
f1mpt.2 
|- ( x = y -> C = D )
Assertion f1mpt 
|- ( F : A -1-1-> B <-> ( A. x e. A C e. B /\ A. x e. A A. y e. A ( C = D -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 f1mpt.1 
 |-  F = ( x e. A |-> C )
2 f1mpt.2 
 |-  ( x = y -> C = D )
3 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
4 1 3 nfcxfr 
 |-  F/_ x F
5 nfcv 
 |-  F/_ y F
6 4 5 dff13f 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
7 1 fmpt 
 |-  ( A. x e. A C e. B <-> F : A --> B )
8 7 anbi1i 
 |-  ( ( A. x e. A C e. B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
9 2 eleq1d 
 |-  ( x = y -> ( C e. B <-> D e. B ) )
10 9 cbvralvw 
 |-  ( A. x e. A C e. B <-> A. y e. A D e. B )
11 raaanv 
 |-  ( A. x e. A A. y e. A ( C e. B /\ D e. B ) <-> ( A. x e. A C e. B /\ A. y e. A D e. B ) )
12 1 fvmpt2 
 |-  ( ( x e. A /\ C e. B ) -> ( F ` x ) = C )
13 2 1 fvmptg 
 |-  ( ( y e. A /\ D e. B ) -> ( F ` y ) = D )
14 12 13 eqeqan12d 
 |-  ( ( ( x e. A /\ C e. B ) /\ ( y e. A /\ D e. B ) ) -> ( ( F ` x ) = ( F ` y ) <-> C = D ) )
15 14 an4s 
 |-  ( ( ( x e. A /\ y e. A ) /\ ( C e. B /\ D e. B ) ) -> ( ( F ` x ) = ( F ` y ) <-> C = D ) )
16 15 imbi1d 
 |-  ( ( ( x e. A /\ y e. A ) /\ ( C e. B /\ D e. B ) ) -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( C = D -> x = y ) ) )
17 16 ex 
 |-  ( ( x e. A /\ y e. A ) -> ( ( C e. B /\ D e. B ) -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( C = D -> x = y ) ) ) )
18 17 ralimdva 
 |-  ( x e. A -> ( A. y e. A ( C e. B /\ D e. B ) -> A. y e. A ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( C = D -> x = y ) ) ) )
19 ralbi 
 |-  ( A. y e. A ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( C = D -> x = y ) ) -> ( A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. y e. A ( C = D -> x = y ) ) )
20 18 19 syl6 
 |-  ( x e. A -> ( A. y e. A ( C e. B /\ D e. B ) -> ( A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. y e. A ( C = D -> x = y ) ) ) )
21 20 ralimia 
 |-  ( A. x e. A A. y e. A ( C e. B /\ D e. B ) -> A. x e. A ( A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. y e. A ( C = D -> x = y ) ) )
22 ralbi 
 |-  ( A. x e. A ( A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. y e. A ( C = D -> x = y ) ) -> ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A ( C = D -> x = y ) ) )
23 21 22 syl 
 |-  ( A. x e. A A. y e. A ( C e. B /\ D e. B ) -> ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A ( C = D -> x = y ) ) )
24 11 23 sylbir 
 |-  ( ( A. x e. A C e. B /\ A. y e. A D e. B ) -> ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A ( C = D -> x = y ) ) )
25 10 24 sylan2b 
 |-  ( ( A. x e. A C e. B /\ A. x e. A C e. B ) -> ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A ( C = D -> x = y ) ) )
26 25 anidms 
 |-  ( A. x e. A C e. B -> ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A ( C = D -> x = y ) ) )
27 26 pm5.32i 
 |-  ( ( A. x e. A C e. B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) <-> ( A. x e. A C e. B /\ A. x e. A A. y e. A ( C = D -> x = y ) ) )
28 6 8 27 3bitr2i 
 |-  ( F : A -1-1-> B <-> ( A. x e. A C e. B /\ A. x e. A A. y e. A ( C = D -> x = y ) ) )