Metamath Proof Explorer

Theorem vdwlem12

Description: Lemma for vdw . K = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdw.r 
|- ( ph -> R e. Fin )
vdwlem12.f 
|- ( ph -> F : ( 1 ... ( ( # ` R ) + 1 ) ) --> R )
vdwlem12.2 
|- ( ph -> -. 2 MonoAP F )
Assertion vdwlem12 
|- -. ph

Proof

Step Hyp Ref Expression
1 vdw.r 
 |-  ( ph -> R e. Fin )
2 vdwlem12.f 
 |-  ( ph -> F : ( 1 ... ( ( # ` R ) + 1 ) ) --> R )
3 vdwlem12.2 
 |-  ( ph -> -. 2 MonoAP F )
4 hashcl 
 |-  ( R e. Fin -> ( # ` R ) e. NN0 )
5 1 4 syl 
 |-  ( ph -> ( # ` R ) e. NN0 )
6 5 nn0red 
 |-  ( ph -> ( # ` R ) e. RR )
7 6 ltp1d 
 |-  ( ph -> ( # ` R ) < ( ( # ` R ) + 1 ) )
8 nn0p1nn 
 |-  ( ( # ` R ) e. NN0 -> ( ( # ` R ) + 1 ) e. NN )
9 5 8 syl 
 |-  ( ph -> ( ( # ` R ) + 1 ) e. NN )
10 9 nnnn0d 
 |-  ( ph -> ( ( # ` R ) + 1 ) e. NN0 )
11 hashfz1 
 |-  ( ( ( # ` R ) + 1 ) e. NN0 -> ( # ` ( 1 ... ( ( # ` R ) + 1 ) ) ) = ( ( # ` R ) + 1 ) )
12 10 11 syl 
 |-  ( ph -> ( # ` ( 1 ... ( ( # ` R ) + 1 ) ) ) = ( ( # ` R ) + 1 ) )
13 7 12 breqtrrd 
 |-  ( ph -> ( # ` R ) < ( # ` ( 1 ... ( ( # ` R ) + 1 ) ) ) )
14 fzfi 
 |-  ( 1 ... ( ( # ` R ) + 1 ) ) e. Fin
15 hashsdom 
 |-  ( ( R e. Fin /\ ( 1 ... ( ( # ` R ) + 1 ) ) e. Fin ) -> ( ( # ` R ) < ( # ` ( 1 ... ( ( # ` R ) + 1 ) ) ) <-> R ~< ( 1 ... ( ( # ` R ) + 1 ) ) ) )
16 1 14 15 sylancl 
 |-  ( ph -> ( ( # ` R ) < ( # ` ( 1 ... ( ( # ` R ) + 1 ) ) ) <-> R ~< ( 1 ... ( ( # ` R ) + 1 ) ) ) )
17 13 16 mpbid 
 |-  ( ph -> R ~< ( 1 ... ( ( # ` R ) + 1 ) ) )
18 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
19 fveq2 
 |-  ( w = y -> ( F ` w ) = ( F ` y ) )
20 18 19 eqeqan12d 
 |-  ( ( z = x /\ w = y ) -> ( ( F ` z ) = ( F ` w ) <-> ( F ` x ) = ( F ` y ) ) )
21 eqeq12 
 |-  ( ( z = x /\ w = y ) -> ( z = w <-> x = y ) )
22 20 21 imbi12d 
 |-  ( ( z = x /\ w = y ) -> ( ( ( F ` z ) = ( F ` w ) -> z = w ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
23 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
24 fveq2 
 |-  ( w = x -> ( F ` w ) = ( F ` x ) )
25 23 24 eqeqan12d 
 |-  ( ( z = y /\ w = x ) -> ( ( F ` z ) = ( F ` w ) <-> ( F ` y ) = ( F ` x ) ) )
26 eqcom 
 |-  ( ( F ` y ) = ( F ` x ) <-> ( F ` x ) = ( F ` y ) )
27 25 26 bitrdi 
 |-  ( ( z = y /\ w = x ) -> ( ( F ` z ) = ( F ` w ) <-> ( F ` x ) = ( F ` y ) ) )
28 eqeq12 
 |-  ( ( z = y /\ w = x ) -> ( z = w <-> y = x ) )
29 eqcom 
 |-  ( y = x <-> x = y )
30 28 29 bitrdi 
 |-  ( ( z = y /\ w = x ) -> ( z = w <-> x = y ) )
31 27 30 imbi12d 
 |-  ( ( z = y /\ w = x ) -> ( ( ( F ` z ) = ( F ` w ) -> z = w ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
32 elfznn 
 |-  ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) -> x e. NN )
33 32 nnred 
 |-  ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) -> x e. RR )
34 33 ssriv 
 |-  ( 1 ... ( ( # ` R ) + 1 ) ) C_ RR
35 34 a1i 
 |-  ( ph -> ( 1 ... ( ( # ` R ) + 1 ) ) C_ RR )
36 biidd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
37 simplr3 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> x <_ y )
38 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> -. 2 MonoAP F )
39 3simpa 
 |-  ( ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) -> ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) )
40 simplrl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> x e. ( 1 ... ( ( # ` R ) + 1 ) ) )
41 40 32 syl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> x e. NN )
42 simprr 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> x < y )
43 simplrr 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> y e. ( 1 ... ( ( # ` R ) + 1 ) ) )
44 elfznn 
 |-  ( y e. ( 1 ... ( ( # ` R ) + 1 ) ) -> y e. NN )
45 43 44 syl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> y e. NN )
46 nnsub 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x < y <-> ( y - x ) e. NN ) )
47 41 45 46 syl2anc 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( x < y <-> ( y - x ) e. NN ) )
48 42 47 mpbid 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( y - x ) e. NN )
49 df-2 
 |-  2 = ( 1 + 1 )
50 49 fveq2i 
 |-  ( AP ` 2 ) = ( AP ` ( 1 + 1 ) )
51 50 oveqi 
 |-  ( x ( AP ` 2 ) ( y - x ) ) = ( x ( AP ` ( 1 + 1 ) ) ( y - x ) )
52 1nn0 
 |-  1 e. NN0
53 vdwapun 
 |-  ( ( 1 e. NN0 /\ x e. NN /\ ( y - x ) e. NN ) -> ( x ( AP ` ( 1 + 1 ) ) ( y - x ) ) = ( { x } u. ( ( x + ( y - x ) ) ( AP ` 1 ) ( y - x ) ) ) )
54 52 41 48 53 mp3an2i 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( x ( AP ` ( 1 + 1 ) ) ( y - x ) ) = ( { x } u. ( ( x + ( y - x ) ) ( AP ` 1 ) ( y - x ) ) ) )
55 51 54 syl5eq 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( x ( AP ` 2 ) ( y - x ) ) = ( { x } u. ( ( x + ( y - x ) ) ( AP ` 1 ) ( y - x ) ) ) )
56 simprl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( F ` x ) = ( F ` y ) )
57 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> F : ( 1 ... ( ( # ` R ) + 1 ) ) --> R )
58 57 ffnd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> F Fn ( 1 ... ( ( # ` R ) + 1 ) ) )
59 fniniseg 
 |-  ( F Fn ( 1 ... ( ( # ` R ) + 1 ) ) -> ( x e. ( `' F " { ( F ` y ) } ) <-> ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ ( F ` x ) = ( F ` y ) ) ) )
60 58 59 syl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( x e. ( `' F " { ( F ` y ) } ) <-> ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ ( F ` x ) = ( F ` y ) ) ) )
61 40 56 60 mpbir2and 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> x e. ( `' F " { ( F ` y ) } ) )
62 61 snssd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> { x } C_ ( `' F " { ( F ` y ) } ) )
63 41 nncnd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> x e. CC )
64 45 nncnd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> y e. CC )
65 63 64 pncan3d 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( x + ( y - x ) ) = y )
66 65 oveq1d 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( ( x + ( y - x ) ) ( AP ` 1 ) ( y - x ) ) = ( y ( AP ` 1 ) ( y - x ) ) )
67 vdwap1 
 |-  ( ( y e. NN /\ ( y - x ) e. NN ) -> ( y ( AP ` 1 ) ( y - x ) ) = { y } )
68 45 48 67 syl2anc 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( y ( AP ` 1 ) ( y - x ) ) = { y } )
69 66 68 eqtrd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( ( x + ( y - x ) ) ( AP ` 1 ) ( y - x ) ) = { y } )
70 eqidd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( F ` y ) = ( F ` y ) )
71 fniniseg 
 |-  ( F Fn ( 1 ... ( ( # ` R ) + 1 ) ) -> ( y e. ( `' F " { ( F ` y ) } ) <-> ( y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ ( F ` y ) = ( F ` y ) ) ) )
72 58 71 syl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( y e. ( `' F " { ( F ` y ) } ) <-> ( y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ ( F ` y ) = ( F ` y ) ) ) )
73 43 70 72 mpbir2and 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> y e. ( `' F " { ( F ` y ) } ) )
74 73 snssd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> { y } C_ ( `' F " { ( F ` y ) } ) )
75 69 74 eqsstrd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( ( x + ( y - x ) ) ( AP ` 1 ) ( y - x ) ) C_ ( `' F " { ( F ` y ) } ) )
76 62 75 unssd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( { x } u. ( ( x + ( y - x ) ) ( AP ` 1 ) ( y - x ) ) ) C_ ( `' F " { ( F ` y ) } ) )
77 55 76 eqsstrd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( x ( AP ` 2 ) ( y - x ) ) C_ ( `' F " { ( F ` y ) } ) )
78 oveq1 
 |-  ( a = x -> ( a ( AP ` 2 ) d ) = ( x ( AP ` 2 ) d ) )
79 78 sseq1d 
 |-  ( a = x -> ( ( a ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) <-> ( x ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) ) )
80 oveq2 
 |-  ( d = ( y - x ) -> ( x ( AP ` 2 ) d ) = ( x ( AP ` 2 ) ( y - x ) ) )
81 80 sseq1d 
 |-  ( d = ( y - x ) -> ( ( x ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) <-> ( x ( AP ` 2 ) ( y - x ) ) C_ ( `' F " { ( F ` y ) } ) ) )
82 79 81 rspc2ev 
 |-  ( ( x e. NN /\ ( y - x ) e. NN /\ ( x ( AP ` 2 ) ( y - x ) ) C_ ( `' F " { ( F ` y ) } ) ) -> E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) )
83 41 48 77 82 syl3anc 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) )
84 fvex 
 |-  ( F ` y ) e. _V
85 sneq 
 |-  ( c = ( F ` y ) -> { c } = { ( F ` y ) } )
86 85 imaeq2d 
 |-  ( c = ( F ` y ) -> ( `' F " { c } ) = ( `' F " { ( F ` y ) } ) )
87 86 sseq2d 
 |-  ( c = ( F ` y ) -> ( ( a ( AP ` 2 ) d ) C_ ( `' F " { c } ) <-> ( a ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) ) )
88 87 2rexbidv 
 |-  ( c = ( F ` y ) -> ( E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { c } ) <-> E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) ) )
89 84 88 spcev 
 |-  ( E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { ( F ` y ) } ) -> E. c E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { c } ) )
90 83 89 syl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> E. c E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { c } ) )
91 ovex 
 |-  ( 1 ... ( ( # ` R ) + 1 ) ) e. _V
92 2nn0 
 |-  2 e. NN0
93 92 a1i 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> 2 e. NN0 )
94 91 93 57 vdwmc 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> ( 2 MonoAP F <-> E. c E. a e. NN E. d e. NN ( a ( AP ` 2 ) d ) C_ ( `' F " { c } ) ) )
95 90 94 mpbird 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> 2 MonoAP F )
96 39 95 sylanl2 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x < y ) ) -> 2 MonoAP F )
97 96 expr 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( x < y -> 2 MonoAP F ) )
98 38 97 mtod 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> -. x < y )
99 simplr1 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> x e. ( 1 ... ( ( # ` R ) + 1 ) ) )
100 99 33 syl 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> x e. RR )
101 simplr2 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> y e. ( 1 ... ( ( # ` R ) + 1 ) ) )
102 34 101 sseldi 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> y e. RR )
103 100 102 eqleltd 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( x = y <-> ( x <_ y /\ -. x < y ) ) )
104 37 98 103 mpbir2and 
 |-  ( ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
105 104 ex 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ x <_ y ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
106 22 31 35 36 105 wlogle 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( # ` R ) + 1 ) ) /\ y e. ( 1 ... ( ( # ` R ) + 1 ) ) ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
107 106 ralrimivva 
 |-  ( ph -> A. x e. ( 1 ... ( ( # ` R ) + 1 ) ) A. y e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) )
108 dff13 
 |-  ( F : ( 1 ... ( ( # ` R ) + 1 ) ) -1-1-> R <-> ( F : ( 1 ... ( ( # ` R ) + 1 ) ) --> R /\ A. x e. ( 1 ... ( ( # ` R ) + 1 ) ) A. y e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
109 2 107 108 sylanbrc 
 |-  ( ph -> F : ( 1 ... ( ( # ` R ) + 1 ) ) -1-1-> R )
110 f1domg 
 |-  ( R e. Fin -> ( F : ( 1 ... ( ( # ` R ) + 1 ) ) -1-1-> R -> ( 1 ... ( ( # ` R ) + 1 ) ) ~<_ R ) )
111 1 109 110 sylc 
 |-  ( ph -> ( 1 ... ( ( # ` R ) + 1 ) ) ~<_ R )
112 domnsym 
 |-  ( ( 1 ... ( ( # ` R ) + 1 ) ) ~<_ R -> -. R ~< ( 1 ... ( ( # ` R ) + 1 ) ) )
113 111 112 syl 
 |-  ( ph -> -. R ~< ( 1 ... ( ( # ` R ) + 1 ) ) )
114 17 113 pm2.65i 
 |-  -. ph