Metamath Proof Explorer

Theorem dom2lem

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004)

Ref Expression
Hypotheses dom2d.1 
|- ( ph -> ( x e. A -> C e. B ) )
dom2d.2 
|- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )
Assertion dom2lem 
|- ( ph -> ( x e. A |-> C ) : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 dom2d.1 
 |-  ( ph -> ( x e. A -> C e. B ) )
2 dom2d.2 
 |-  ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )
3 1 ralrimiv 
 |-  ( ph -> A. x e. A C e. B )
4 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
5 4 fmpt 
 |-  ( A. x e. A C e. B <-> ( x e. A |-> C ) : A --> B )
6 3 5 sylib 
 |-  ( ph -> ( x e. A |-> C ) : A --> B )
7 1 imp 
 |-  ( ( ph /\ x e. A ) -> C e. B )
8 4 fvmpt2 
 |-  ( ( x e. A /\ C e. B ) -> ( ( x e. A |-> C ) ` x ) = C )
9 8 adantll 
 |-  ( ( ( ph /\ x e. A ) /\ C e. B ) -> ( ( x e. A |-> C ) ` x ) = C )
10 7 9 mpdan 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> C ) ` x ) = C )
11 10 adantrr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( x e. A |-> C ) ` x ) = C )
12 nfv 
 |-  F/ x ( ph /\ y e. A )
13 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> C ) ` y )
14 13 nfeq1 
 |-  F/ x ( ( x e. A |-> C ) ` y ) = D
15 12 14 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> ( ( x e. A |-> C ) ` y ) = D )
16 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
17 16 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. A ) <-> ( ph /\ y e. A ) ) )
18 17 imbi1d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> ( ( x e. A |-> C ) ` x ) = C ) <-> ( ( ph /\ y e. A ) -> ( ( x e. A |-> C ) ` x ) = C ) ) )
19 16 anbi1d 
 |-  ( x = y -> ( ( x e. A /\ y e. A ) <-> ( y e. A /\ y e. A ) ) )
20 anidm 
 |-  ( ( y e. A /\ y e. A ) <-> y e. A )
21 19 20 bitrdi 
 |-  ( x = y -> ( ( x e. A /\ y e. A ) <-> y e. A ) )
22 21 anbi2d 
 |-  ( x = y -> ( ( ph /\ ( x e. A /\ y e. A ) ) <-> ( ph /\ y e. A ) ) )
23 fveq2 
 |-  ( x = y -> ( ( x e. A |-> C ) ` x ) = ( ( x e. A |-> C ) ` y ) )
24 23 adantr 
 |-  ( ( x = y /\ ( ph /\ ( x e. A /\ y e. A ) ) ) -> ( ( x e. A |-> C ) ` x ) = ( ( x e. A |-> C ) ` y ) )
25 2 imp 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( C = D <-> x = y ) )
26 25 biimparc 
 |-  ( ( x = y /\ ( ph /\ ( x e. A /\ y e. A ) ) ) -> C = D )
27 24 26 eqeq12d 
 |-  ( ( x = y /\ ( ph /\ ( x e. A /\ y e. A ) ) ) -> ( ( ( x e. A |-> C ) ` x ) = C <-> ( ( x e. A |-> C ) ` y ) = D ) )
28 27 ex 
 |-  ( x = y -> ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( ( x e. A |-> C ) ` x ) = C <-> ( ( x e. A |-> C ) ` y ) = D ) ) )
29 22 28 sylbird 
 |-  ( x = y -> ( ( ph /\ y e. A ) -> ( ( ( x e. A |-> C ) ` x ) = C <-> ( ( x e. A |-> C ) ` y ) = D ) ) )
30 29 pm5.74d 
 |-  ( x = y -> ( ( ( ph /\ y e. A ) -> ( ( x e. A |-> C ) ` x ) = C ) <-> ( ( ph /\ y e. A ) -> ( ( x e. A |-> C ) ` y ) = D ) ) )
31 18 30 bitrd 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> ( ( x e. A |-> C ) ` x ) = C ) <-> ( ( ph /\ y e. A ) -> ( ( x e. A |-> C ) ` y ) = D ) ) )
32 15 31 10 chvarfv 
 |-  ( ( ph /\ y e. A ) -> ( ( x e. A |-> C ) ` y ) = D )
33 32 adantrl 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( x e. A |-> C ) ` y ) = D )
34 11 33 eqeq12d 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( ( x e. A |-> C ) ` x ) = ( ( x e. A |-> C ) ` y ) <-> C = D ) )
35 25 biimpd 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( C = D -> x = y ) )
36 34 35 sylbid 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( ( x e. A |-> C ) ` x ) = ( ( x e. A |-> C ) ` y ) -> x = y ) )
37 36 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. A ( ( ( x e. A |-> C ) ` x ) = ( ( x e. A |-> C ) ` y ) -> x = y ) )
38 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
39 nfcv 
 |-  F/_ y ( x e. A |-> C )
40 38 39 dff13f 
 |-  ( ( x e. A |-> C ) : A -1-1-> B <-> ( ( x e. A |-> C ) : A --> B /\ A. x e. A A. y e. A ( ( ( x e. A |-> C ) ` x ) = ( ( x e. A |-> C ) ` y ) -> x = y ) ) )
41 6 37 40 sylanbrc 
 |-  ( ph -> ( x e. A |-> C ) : A -1-1-> B )