Metamath Proof Explorer

Theorem fphpd

Description: Pigeonhole principle expressed with implicit substitution. If the range is smaller than the domain, two inputs must be mapped to the same output. (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses fphpd.a 
|- ( ph -> B ~< A )
fphpd.b 
|- ( ( ph /\ x e. A ) -> C e. B )
fphpd.c 
|- ( x = y -> C = D )
Assertion fphpd 
|- ( ph -> E. x e. A E. y e. A ( x =/= y /\ C = D ) )

Proof

Step Hyp Ref Expression
1 fphpd.a 
 |-  ( ph -> B ~< A )
2 fphpd.b 
 |-  ( ( ph /\ x e. A ) -> C e. B )
3 fphpd.c 
 |-  ( x = y -> C = D )
4 domnsym 
 |-  ( A ~<_ B -> -. B ~< A )
5 4 1 nsyl3 
 |-  ( ph -> -. A ~<_ B )
6 relsdom 
 |-  Rel ~<
7 6 brrelex1i 
 |-  ( B ~< A -> B e. _V )
8 1 7 syl 
 |-  ( ph -> B e. _V )
9 8 adantr 
 |-  ( ( ph /\ A. x e. A A. y e. A ( C = D -> x = y ) ) -> B e. _V )
10 nfv 
 |-  F/ x ( ph /\ a e. A )
11 nfcsb1v 
 |-  F/_ x [_ a / x ]_ C
12 11 nfel1 
 |-  F/ x [_ a / x ]_ C e. B
13 10 12 nfim 
 |-  F/ x ( ( ph /\ a e. A ) -> [_ a / x ]_ C e. B )
14 eleq1w 
 |-  ( x = a -> ( x e. A <-> a e. A ) )
15 14 anbi2d 
 |-  ( x = a -> ( ( ph /\ x e. A ) <-> ( ph /\ a e. A ) ) )
16 csbeq1a 
 |-  ( x = a -> C = [_ a / x ]_ C )
17 16 eleq1d 
 |-  ( x = a -> ( C e. B <-> [_ a / x ]_ C e. B ) )
18 15 17 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. A ) -> C e. B ) <-> ( ( ph /\ a e. A ) -> [_ a / x ]_ C e. B ) ) )
19 13 18 2 chvarfv 
 |-  ( ( ph /\ a e. A ) -> [_ a / x ]_ C e. B )
20 19 ex 
 |-  ( ph -> ( a e. A -> [_ a / x ]_ C e. B ) )
21 20 adantr 
 |-  ( ( ph /\ A. x e. A A. y e. A ( C = D -> x = y ) ) -> ( a e. A -> [_ a / x ]_ C e. B ) )
22 csbid 
 |-  [_ x / x ]_ C = C
23 vex 
 |-  y e. _V
24 23 3 csbie 
 |-  [_ y / x ]_ C = D
25 22 24 eqeq12i 
 |-  ( [_ x / x ]_ C = [_ y / x ]_ C <-> C = D )
26 25 imbi1i 
 |-  ( ( [_ x / x ]_ C = [_ y / x ]_ C -> x = y ) <-> ( C = D -> x = y ) )
27 26 2ralbii 
 |-  ( A. x e. A A. y e. A ( [_ x / x ]_ C = [_ y / x ]_ C -> x = y ) <-> A. x e. A A. y e. A ( C = D -> x = y ) )
28 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
29 11 28 nfeq 
 |-  F/ x [_ a / x ]_ C = [_ y / x ]_ C
30 nfv 
 |-  F/ x a = y
31 29 30 nfim 
 |-  F/ x ( [_ a / x ]_ C = [_ y / x ]_ C -> a = y )
32 nfv 
 |-  F/ y ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b )
33 csbeq1 
 |-  ( x = a -> [_ x / x ]_ C = [_ a / x ]_ C )
34 33 eqeq1d 
 |-  ( x = a -> ( [_ x / x ]_ C = [_ y / x ]_ C <-> [_ a / x ]_ C = [_ y / x ]_ C ) )
35 equequ1 
 |-  ( x = a -> ( x = y <-> a = y ) )
36 34 35 imbi12d 
 |-  ( x = a -> ( ( [_ x / x ]_ C = [_ y / x ]_ C -> x = y ) <-> ( [_ a / x ]_ C = [_ y / x ]_ C -> a = y ) ) )
37 csbeq1 
 |-  ( y = b -> [_ y / x ]_ C = [_ b / x ]_ C )
38 37 eqeq2d 
 |-  ( y = b -> ( [_ a / x ]_ C = [_ y / x ]_ C <-> [_ a / x ]_ C = [_ b / x ]_ C ) )
39 equequ2 
 |-  ( y = b -> ( a = y <-> a = b ) )
40 38 39 imbi12d 
 |-  ( y = b -> ( ( [_ a / x ]_ C = [_ y / x ]_ C -> a = y ) <-> ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b ) ) )
41 31 32 36 40 rspc2 
 |-  ( ( a e. A /\ b e. A ) -> ( A. x e. A A. y e. A ( [_ x / x ]_ C = [_ y / x ]_ C -> x = y ) -> ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b ) ) )
42 41 com12 
 |-  ( A. x e. A A. y e. A ( [_ x / x ]_ C = [_ y / x ]_ C -> x = y ) -> ( ( a e. A /\ b e. A ) -> ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b ) ) )
43 27 42 sylbir 
 |-  ( A. x e. A A. y e. A ( C = D -> x = y ) -> ( ( a e. A /\ b e. A ) -> ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b ) ) )
44 id 
 |-  ( ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b ) -> ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b ) )
45 csbeq1 
 |-  ( a = b -> [_ a / x ]_ C = [_ b / x ]_ C )
46 44 45 impbid1 
 |-  ( ( [_ a / x ]_ C = [_ b / x ]_ C -> a = b ) -> ( [_ a / x ]_ C = [_ b / x ]_ C <-> a = b ) )
47 43 46 syl6 
 |-  ( A. x e. A A. y e. A ( C = D -> x = y ) -> ( ( a e. A /\ b e. A ) -> ( [_ a / x ]_ C = [_ b / x ]_ C <-> a = b ) ) )
48 47 adantl 
 |-  ( ( ph /\ A. x e. A A. y e. A ( C = D -> x = y ) ) -> ( ( a e. A /\ b e. A ) -> ( [_ a / x ]_ C = [_ b / x ]_ C <-> a = b ) ) )
49 21 48 dom2d 
 |-  ( ( ph /\ A. x e. A A. y e. A ( C = D -> x = y ) ) -> ( B e. _V -> A ~<_ B ) )
50 9 49 mpd 
 |-  ( ( ph /\ A. x e. A A. y e. A ( C = D -> x = y ) ) -> A ~<_ B )
51 5 50 mtand 
 |-  ( ph -> -. A. x e. A A. y e. A ( C = D -> x = y ) )
52 ancom 
 |-  ( ( -. x = y /\ C = D ) <-> ( C = D /\ -. x = y ) )
53 df-ne 
 |-  ( x =/= y <-> -. x = y )
54 53 anbi1i 
 |-  ( ( x =/= y /\ C = D ) <-> ( -. x = y /\ C = D ) )
55 pm4.61 
 |-  ( -. ( C = D -> x = y ) <-> ( C = D /\ -. x = y ) )
56 52 54 55 3bitr4i 
 |-  ( ( x =/= y /\ C = D ) <-> -. ( C = D -> x = y ) )
57 56 rexbii 
 |-  ( E. y e. A ( x =/= y /\ C = D ) <-> E. y e. A -. ( C = D -> x = y ) )
58 rexnal 
 |-  ( E. y e. A -. ( C = D -> x = y ) <-> -. A. y e. A ( C = D -> x = y ) )
59 57 58 bitri 
 |-  ( E. y e. A ( x =/= y /\ C = D ) <-> -. A. y e. A ( C = D -> x = y ) )
60 59 rexbii 
 |-  ( E. x e. A E. y e. A ( x =/= y /\ C = D ) <-> E. x e. A -. A. y e. A ( C = D -> x = y ) )
61 rexnal 
 |-  ( E. x e. A -. A. y e. A ( C = D -> x = y ) <-> -. A. x e. A A. y e. A ( C = D -> x = y ) )
62 60 61 bitri 
 |-  ( E. x e. A E. y e. A ( x =/= y /\ C = D ) <-> -. A. x e. A A. y e. A ( C = D -> x = y ) )
63 51 62 sylibr 
 |-  ( ph -> E. x e. A E. y e. A ( x =/= y /\ C = D ) )