Metamath Proof Explorer

Theorem fphpdo

Description: Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Hypotheses fphpdo.1 
|- ( ph -> A C_ RR )
fphpdo.2 
|- ( ph -> B e. _V )
fphpdo.3 
|- ( ph -> B ~< A )
fphpdo.4 
|- ( ( ph /\ z e. A ) -> C e. B )
fphpdo.5 
|- ( z = x -> C = D )
fphpdo.6 
|- ( z = y -> C = E )
Assertion fphpdo 
|- ( ph -> E. x e. A E. y e. A ( x < y /\ D = E ) )

Proof

Step Hyp Ref Expression
1 fphpdo.1 
 |-  ( ph -> A C_ RR )
2 fphpdo.2 
 |-  ( ph -> B e. _V )
3 fphpdo.3 
 |-  ( ph -> B ~< A )
4 fphpdo.4 
 |-  ( ( ph /\ z e. A ) -> C e. B )
5 fphpdo.5 
 |-  ( z = x -> C = D )
6 fphpdo.6 
 |-  ( z = y -> C = E )
7 4 fmpttd 
 |-  ( ph -> ( z e. A |-> C ) : A --> B )
8 7 ffvelrnda 
 |-  ( ( ph /\ b e. A ) -> ( ( z e. A |-> C ) ` b ) e. B )
9 fveq2 
 |-  ( b = c -> ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) )
10 3 8 9 fphpd 
 |-  ( ph -> E. b e. A E. c e. A ( b =/= c /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) )
11 1 sselda 
 |-  ( ( ph /\ b e. A ) -> b e. RR )
12 11 adantrr 
 |-  ( ( ph /\ ( b e. A /\ c e. A ) ) -> b e. RR )
13 12 adantr 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> b e. RR )
14 1 sselda 
 |-  ( ( ph /\ c e. A ) -> c e. RR )
15 14 adantrl 
 |-  ( ( ph /\ ( b e. A /\ c e. A ) ) -> c e. RR )
16 15 adantr 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> c e. RR )
17 13 16 lttri2d 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> ( b =/= c <-> ( b < c \/ c < b ) ) )
18 simprl 
 |-  ( ( ph /\ ( b e. A /\ c e. A ) ) -> b e. A )
19 18 ad2antrr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ b < c ) -> b e. A )
20 simprr 
 |-  ( ( ph /\ ( b e. A /\ c e. A ) ) -> c e. A )
21 20 ad2antrr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ b < c ) -> c e. A )
22 simpr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ b < c ) -> b < c )
23 simplr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ b < c ) -> ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) )
24 breq1 
 |-  ( x = b -> ( x < y <-> b < y ) )
25 fveqeq2 
 |-  ( x = b -> ( ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) <-> ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` y ) ) )
26 24 25 anbi12d 
 |-  ( x = b -> ( ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) <-> ( b < y /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` y ) ) ) )
27 breq2 
 |-  ( y = c -> ( b < y <-> b < c ) )
28 fveq2 
 |-  ( y = c -> ( ( z e. A |-> C ) ` y ) = ( ( z e. A |-> C ) ` c ) )
29 28 eqeq2d 
 |-  ( y = c -> ( ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` y ) <-> ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) )
30 27 29 anbi12d 
 |-  ( y = c -> ( ( b < y /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` y ) ) <-> ( b < c /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) ) )
31 26 30 rspc2ev 
 |-  ( ( b e. A /\ c e. A /\ ( b < c /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) ) -> E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) )
32 19 21 22 23 31 syl112anc 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ b < c ) -> E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) )
33 32 ex 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> ( b < c -> E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) ) )
34 20 ad2antrr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ c < b ) -> c e. A )
35 18 ad2antrr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ c < b ) -> b e. A )
36 simpr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ c < b ) -> c < b )
37 simplr 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ c < b ) -> ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) )
38 37 eqcomd 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ c < b ) -> ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` b ) )
39 breq1 
 |-  ( x = c -> ( x < y <-> c < y ) )
40 fveqeq2 
 |-  ( x = c -> ( ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) <-> ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` y ) ) )
41 39 40 anbi12d 
 |-  ( x = c -> ( ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) <-> ( c < y /\ ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` y ) ) ) )
42 breq2 
 |-  ( y = b -> ( c < y <-> c < b ) )
43 fveq2 
 |-  ( y = b -> ( ( z e. A |-> C ) ` y ) = ( ( z e. A |-> C ) ` b ) )
44 43 eqeq2d 
 |-  ( y = b -> ( ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` y ) <-> ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` b ) ) )
45 42 44 anbi12d 
 |-  ( y = b -> ( ( c < y /\ ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` y ) ) <-> ( c < b /\ ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` b ) ) ) )
46 41 45 rspc2ev 
 |-  ( ( c e. A /\ b e. A /\ ( c < b /\ ( ( z e. A |-> C ) ` c ) = ( ( z e. A |-> C ) ` b ) ) ) -> E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) )
47 34 35 36 38 46 syl112anc 
 |-  ( ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) /\ c < b ) -> E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) )
48 47 ex 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> ( c < b -> E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) ) )
49 33 48 jaod 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> ( ( b < c \/ c < b ) -> E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) ) )
50 eqid 
 |-  ( z e. A |-> C ) = ( z e. A |-> C )
51 simplr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> x e. A )
52 eleq1w 
 |-  ( z = x -> ( z e. A <-> x e. A ) )
53 52 anbi2d 
 |-  ( z = x -> ( ( ph /\ z e. A ) <-> ( ph /\ x e. A ) ) )
54 5 eleq1d 
 |-  ( z = x -> ( C e. B <-> D e. B ) )
55 53 54 imbi12d 
 |-  ( z = x -> ( ( ( ph /\ z e. A ) -> C e. B ) <-> ( ( ph /\ x e. A ) -> D e. B ) ) )
56 55 4 chvarvv 
 |-  ( ( ph /\ x e. A ) -> D e. B )
57 56 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> D e. B )
58 50 5 51 57 fvmptd3 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( ( z e. A |-> C ) ` x ) = D )
59 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> y e. A )
60 eleq1w 
 |-  ( z = y -> ( z e. A <-> y e. A ) )
61 60 anbi2d 
 |-  ( z = y -> ( ( ph /\ z e. A ) <-> ( ph /\ y e. A ) ) )
62 6 eleq1d 
 |-  ( z = y -> ( C e. B <-> E e. B ) )
63 61 62 imbi12d 
 |-  ( z = y -> ( ( ( ph /\ z e. A ) -> C e. B ) <-> ( ( ph /\ y e. A ) -> E e. B ) ) )
64 63 4 chvarvv 
 |-  ( ( ph /\ y e. A ) -> E e. B )
65 64 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> E e. B )
66 50 6 59 65 fvmptd3 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( ( z e. A |-> C ) ` y ) = E )
67 58 66 eqeq12d 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) <-> D = E ) )
68 67 biimpd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) -> D = E ) )
69 68 anim2d 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) -> ( x < y /\ D = E ) ) )
70 69 reximdva 
 |-  ( ( ph /\ x e. A ) -> ( E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) -> E. y e. A ( x < y /\ D = E ) ) )
71 70 reximdva 
 |-  ( ph -> ( E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) -> E. x e. A E. y e. A ( x < y /\ D = E ) ) )
72 71 ad2antrr 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> ( E. x e. A E. y e. A ( x < y /\ ( ( z e. A |-> C ) ` x ) = ( ( z e. A |-> C ) ` y ) ) -> E. x e. A E. y e. A ( x < y /\ D = E ) ) )
73 49 72 syld 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> ( ( b < c \/ c < b ) -> E. x e. A E. y e. A ( x < y /\ D = E ) ) )
74 17 73 sylbid 
 |-  ( ( ( ph /\ ( b e. A /\ c e. A ) ) /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> ( b =/= c -> E. x e. A E. y e. A ( x < y /\ D = E ) ) )
75 74 expimpd 
 |-  ( ( ph /\ ( b e. A /\ c e. A ) ) -> ( ( ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) /\ b =/= c ) -> E. x e. A E. y e. A ( x < y /\ D = E ) ) )
76 75 ancomsd 
 |-  ( ( ph /\ ( b e. A /\ c e. A ) ) -> ( ( b =/= c /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> E. x e. A E. y e. A ( x < y /\ D = E ) ) )
77 76 rexlimdvva 
 |-  ( ph -> ( E. b e. A E. c e. A ( b =/= c /\ ( ( z e. A |-> C ) ` b ) = ( ( z e. A |-> C ) ` c ) ) -> E. x e. A E. y e. A ( x < y /\ D = E ) ) )
78 10 77 mpd 
 |-  ( ph -> E. x e. A E. y e. A ( x < y /\ D = E ) )