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 )