Metamath Proof Explorer

Theorem sticksstones1

Description: Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024)

Ref Expression
Hypotheses sticksstones1.1 
|- ( ph -> N e. NN0 )
sticksstones1.2 
|- ( ph -> K e. NN0 )
sticksstones1.3 
|- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
sticksstones1.4 
|- ( ph -> X e. A )
sticksstones1.5 
|- ( ph -> Y e. A )
sticksstones1.6 
|- ( ph -> X =/= Y )
sticksstones1.7 
|- I = inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < )
Assertion sticksstones1 
|- ( ph -> ran X =/= ran Y )

Proof

Step Hyp Ref Expression
1 sticksstones1.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones1.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones1.3 
 |-  A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
4 sticksstones1.4 
 |-  ( ph -> X e. A )
5 sticksstones1.5 
 |-  ( ph -> Y e. A )
6 sticksstones1.6 
 |-  ( ph -> X =/= Y )
7 sticksstones1.7 
 |-  I = inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < )
8 7 a1i 
 |-  ( ph -> I = inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) )
9 ltso 
 |-  < Or RR
10 9 a1i 
 |-  ( ph -> < Or RR )
11 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
12 ssrab2 
 |-  { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ ( 1 ... K )
13 12 a1i 
 |-  ( ph -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ ( 1 ... K ) )
14 ssfi 
 |-  ( ( ( 1 ... K ) e. Fin /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ ( 1 ... K ) ) -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } e. Fin )
15 11 13 14 syl2anc 
 |-  ( ph -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } e. Fin )
16 rabeq0 
 |-  ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } = (/) <-> A. z e. ( 1 ... K ) -. ( X ` z ) =/= ( Y ` z ) )
17 nne 
 |-  ( -. ( X ` z ) =/= ( Y ` z ) <-> ( X ` z ) = ( Y ` z ) )
18 17 ralbii 
 |-  ( A. z e. ( 1 ... K ) -. ( X ` z ) =/= ( Y ` z ) <-> A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) )
19 16 18 bitri 
 |-  ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } = (/) <-> A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) )
20 feq1 
 |-  ( f = X -> ( f : ( 1 ... K ) --> ( 1 ... N ) <-> X : ( 1 ... K ) --> ( 1 ... N ) ) )
21 fveq1 
 |-  ( f = X -> ( f ` x ) = ( X ` x ) )
22 fveq1 
 |-  ( f = X -> ( f ` y ) = ( X ` y ) )
23 21 22 breq12d 
 |-  ( f = X -> ( ( f ` x ) < ( f ` y ) <-> ( X ` x ) < ( X ` y ) ) )
24 23 imbi2d 
 |-  ( f = X -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( X ` x ) < ( X ` y ) ) ) )
25 24 2ralbidv 
 |-  ( f = X -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) <-> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) ) )
26 20 25 anbi12d 
 |-  ( f = X -> ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( X : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) ) ) )
27 eqabb 
 |-  ( A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } <-> A. f ( f e. A <-> ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) ) )
28 3 27 mpbi 
 |-  A. f ( f e. A <-> ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) )
29 28 spi 
 |-  ( f e. A <-> ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) )
30 29 bilani 
 |-  ( ( ph /\ f e. A ) -> ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) )
31 30 ralrimiva 
 |-  ( ph -> A. f e. A ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) )
32 26 31 4 rspcdva 
 |-  ( ph -> ( X : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) ) )
33 32 simpld 
 |-  ( ph -> X : ( 1 ... K ) --> ( 1 ... N ) )
34 33 ffnd 
 |-  ( ph -> X Fn ( 1 ... K ) )
35 34 adantr 
 |-  ( ( ph /\ A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) -> X Fn ( 1 ... K ) )
36 feq1 
 |-  ( f = Y -> ( f : ( 1 ... K ) --> ( 1 ... N ) <-> Y : ( 1 ... K ) --> ( 1 ... N ) ) )
37 fveq1 
 |-  ( f = Y -> ( f ` x ) = ( Y ` x ) )
38 fveq1 
 |-  ( f = Y -> ( f ` y ) = ( Y ` y ) )
39 37 38 breq12d 
 |-  ( f = Y -> ( ( f ` x ) < ( f ` y ) <-> ( Y ` x ) < ( Y ` y ) ) )
40 39 imbi2d 
 |-  ( f = Y -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( Y ` x ) < ( Y ` y ) ) ) )
41 40 2ralbidv 
 |-  ( f = Y -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) <-> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) ) )
42 36 41 anbi12d 
 |-  ( f = Y -> ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( Y : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) ) ) )
43 42 31 5 rspcdva 
 |-  ( ph -> ( Y : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) ) )
44 43 adantr 
 |-  ( ( ph /\ Y e. A ) -> ( Y : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) ) )
45 5 44 mpdan 
 |-  ( ph -> ( Y : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) ) )
46 45 simpld 
 |-  ( ph -> Y : ( 1 ... K ) --> ( 1 ... N ) )
47 46 ffnd 
 |-  ( ph -> Y Fn ( 1 ... K ) )
48 47 adantr 
 |-  ( ( ph /\ A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) -> Y Fn ( 1 ... K ) )
49 eqfnfv 
 |-  ( ( X Fn ( 1 ... K ) /\ Y Fn ( 1 ... K ) ) -> ( X = Y <-> A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) )
50 35 48 49 syl2anc 
 |-  ( ( ph /\ A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) -> ( X = Y <-> A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) )
51 50 bicomd 
 |-  ( ( ph /\ A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) -> ( A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) <-> X = Y ) )
52 51 biimpd 
 |-  ( ( ph /\ A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) -> ( A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) -> X = Y ) )
53 52 syldbl2 
 |-  ( ( ph /\ A. z e. ( 1 ... K ) ( X ` z ) = ( Y ` z ) ) -> X = Y )
54 19 53 sylan2b 
 |-  ( ( ph /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } = (/) ) -> X = Y )
55 54 ex 
 |-  ( ph -> ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } = (/) -> X = Y ) )
56 55 necon3d 
 |-  ( ph -> ( X =/= Y -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } =/= (/) ) )
57 56 imp 
 |-  ( ( ph /\ X =/= Y ) -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } =/= (/) )
58 6 57 mpdan 
 |-  ( ph -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } =/= (/) )
59 fz1ssnn 
 |-  ( 1 ... K ) C_ NN
60 59 a1i 
 |-  ( ph -> ( 1 ... K ) C_ NN )
61 nnssre 
 |-  NN C_ RR
62 61 a1i 
 |-  ( ph -> NN C_ RR )
63 60 62 sstrd 
 |-  ( ph -> ( 1 ... K ) C_ RR )
64 13 63 sstrd 
 |-  ( ph -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ RR )
65 15 58 64 3jca 
 |-  ( ph -> ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } e. Fin /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } =/= (/) /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ RR ) )
66 fiinfcl 
 |-  ( ( < Or RR /\ ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } e. Fin /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } =/= (/) /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ RR ) ) -> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } )
67 10 65 66 syl2anc 
 |-  ( ph -> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } )
68 8 67 eqeltrd 
 |-  ( ph -> I e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } )
69 13 67 sseldd 
 |-  ( ph -> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) e. ( 1 ... K ) )
70 8 eleq1d 
 |-  ( ph -> ( I e. ( 1 ... K ) <-> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) e. ( 1 ... K ) ) )
71 69 70 mpbird 
 |-  ( ph -> I e. ( 1 ... K ) )
72 fveq2 
 |-  ( z = I -> ( X ` z ) = ( X ` I ) )
73 fveq2 
 |-  ( z = I -> ( Y ` z ) = ( Y ` I ) )
74 72 73 neeq12d 
 |-  ( z = I -> ( ( X ` z ) =/= ( Y ` z ) <-> ( X ` I ) =/= ( Y ` I ) ) )
75 74 elrab3 
 |-  ( I e. ( 1 ... K ) -> ( I e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } <-> ( X ` I ) =/= ( Y ` I ) ) )
76 71 75 syl 
 |-  ( ph -> ( I e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } <-> ( X ` I ) =/= ( Y ` I ) ) )
77 68 76 mpbid 
 |-  ( ph -> ( X ` I ) =/= ( Y ` I ) )
78 nfv 
 |-  F/ a ph
79 nfcv 
 |-  F/_ a ( 1 ... N )
80 nfcv 
 |-  F/_ a RR
81 elfznn 
 |-  ( a e. ( 1 ... N ) -> a e. NN )
82 81 adantl 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> a e. NN )
83 nnre 
 |-  ( a e. NN -> a e. RR )
84 82 83 syl 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> a e. RR )
85 84 ex 
 |-  ( ph -> ( a e. ( 1 ... N ) -> a e. RR ) )
86 78 79 80 85 ssrd 
 |-  ( ph -> ( 1 ... N ) C_ RR )
87 33 71 ffvelcdmd 
 |-  ( ph -> ( X ` I ) e. ( 1 ... N ) )
88 86 87 sseldd 
 |-  ( ph -> ( X ` I ) e. RR )
89 46 71 ffvelcdmd 
 |-  ( ph -> ( Y ` I ) e. ( 1 ... N ) )
90 86 89 sseldd 
 |-  ( ph -> ( Y ` I ) e. RR )
91 lttri2 
 |-  ( ( ( X ` I ) e. RR /\ ( Y ` I ) e. RR ) -> ( ( X ` I ) =/= ( Y ` I ) <-> ( ( X ` I ) < ( Y ` I ) \/ ( Y ` I ) < ( X ` I ) ) ) )
92 88 90 91 syl2anc 
 |-  ( ph -> ( ( X ` I ) =/= ( Y ` I ) <-> ( ( X ` I ) < ( Y ` I ) \/ ( Y ` I ) < ( X ` I ) ) ) )
93 77 92 mpbid 
 |-  ( ph -> ( ( X ` I ) < ( Y ` I ) \/ ( Y ` I ) < ( X ` I ) ) )
94 33 ffund 
 |-  ( ph -> Fun X )
95 94 adantr 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) ) -> Fun X )
96 33 fdmd 
 |-  ( ph -> dom X = ( 1 ... K ) )
97 71 96 eleqtrrd 
 |-  ( ph -> I e. dom X )
98 97 adantr 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) ) -> I e. dom X )
99 fvelrn 
 |-  ( ( Fun X /\ I e. dom X ) -> ( X ` I ) e. ran X )
100 95 98 99 syl2anc 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) ) -> ( X ` I ) e. ran X )
101 elfznn 
 |-  ( j e. ( 1 ... K ) -> j e. NN )
102 101 3ad2ant3 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> j e. NN )
103 102 nnred 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> j e. RR )
104 63 71 sseldd 
 |-  ( ph -> I e. RR )
105 104 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> I e. RR )
106 103 105 lttri4d 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> ( j < I \/ j = I \/ I < j ) )
107 46 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> Y : ( 1 ... K ) --> ( 1 ... N ) )
108 simp3 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> j e. ( 1 ... K ) )
109 107 108 ffvelcdmd 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> ( Y ` j ) e. ( 1 ... N ) )
110 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
111 110 sseli 
 |-  ( ( Y ` j ) e. ( 1 ... N ) -> ( Y ` j ) e. NN )
112 nnre 
 |-  ( ( Y ` j ) e. NN -> ( Y ` j ) e. RR )
113 111 112 syl 
 |-  ( ( Y ` j ) e. ( 1 ... N ) -> ( Y ` j ) e. RR )
114 109 113 syl 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> ( Y ` j ) e. RR )
115 114 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( Y ` j ) e. RR )
116 32 simprd 
 |-  ( ph -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) )
117 116 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) )
118 117 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) )
119 simpl3 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> j e. ( 1 ... K ) )
120 71 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> I e. ( 1 ... K ) )
121 120 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> I e. ( 1 ... K ) )
122 breq1 
 |-  ( x = j -> ( x < y <-> j < y ) )
123 fveq2 
 |-  ( x = j -> ( X ` x ) = ( X ` j ) )
124 123 breq1d 
 |-  ( x = j -> ( ( X ` x ) < ( X ` y ) <-> ( X ` j ) < ( X ` y ) ) )
125 122 124 imbi12d 
 |-  ( x = j -> ( ( x < y -> ( X ` x ) < ( X ` y ) ) <-> ( j < y -> ( X ` j ) < ( X ` y ) ) ) )
126 breq2 
 |-  ( y = I -> ( j < y <-> j < I ) )
127 fveq2 
 |-  ( y = I -> ( X ` y ) = ( X ` I ) )
128 127 breq2d 
 |-  ( y = I -> ( ( X ` j ) < ( X ` y ) <-> ( X ` j ) < ( X ` I ) ) )
129 126 128 imbi12d 
 |-  ( y = I -> ( ( j < y -> ( X ` j ) < ( X ` y ) ) <-> ( j < I -> ( X ` j ) < ( X ` I ) ) ) )
130 125 129 rspc2v 
 |-  ( ( j e. ( 1 ... K ) /\ I e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) -> ( j < I -> ( X ` j ) < ( X ` I ) ) ) )
131 119 121 130 syl2anc 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) -> ( j < I -> ( X ` j ) < ( X ` I ) ) ) )
132 118 131 mpd 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( j < I -> ( X ` j ) < ( X ` I ) ) )
133 132 syldbl2 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( X ` j ) < ( X ` I ) )
134 simp2 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> j e. ( 1 ... K ) )
135 simp3 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> j < I )
136 101 3ad2ant2 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> j e. NN )
137 136 nnred 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> j e. RR )
138 104 3ad2ant1 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> I e. RR )
139 137 138 ltnled 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> ( j < I <-> -. I <_ j ) )
140 135 139 mpbid 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> -. I <_ j )
141 64 3ad2ant1 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ RR )
142 15 3ad2ant1 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } e. Fin )
143 infrefilb 
 |-  ( ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ RR /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } e. Fin /\ j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } ) -> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) <_ j )
144 143 3expia 
 |-  ( ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } C_ RR /\ { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } e. Fin ) -> ( j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } -> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) <_ j ) )
145 141 142 144 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> ( j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } -> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) <_ j ) )
146 145 imp 
 |-  ( ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) /\ j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } ) -> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) <_ j )
147 7 a1i 
 |-  ( ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) /\ j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } ) -> I = inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) )
148 147 breq1d 
 |-  ( ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) /\ j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } ) -> ( I <_ j <-> inf ( { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } , RR , < ) <_ j ) )
149 146 148 mpbird 
 |-  ( ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) /\ j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } ) -> I <_ j )
150 149 ex 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> ( j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } -> I <_ j ) )
151 150 con3d 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> ( -. I <_ j -> -. j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } ) )
152 140 151 mpd 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> -. j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } )
153 nfcv 
 |-  F/_ z j
154 nfcv 
 |-  F/_ z ( 1 ... K )
155 nfv 
 |-  F/ z ( X ` j ) =/= ( Y ` j )
156 fveq2 
 |-  ( z = j -> ( X ` z ) = ( X ` j ) )
157 fveq2 
 |-  ( z = j -> ( Y ` z ) = ( Y ` j ) )
158 156 157 neeq12d 
 |-  ( z = j -> ( ( X ` z ) =/= ( Y ` z ) <-> ( X ` j ) =/= ( Y ` j ) ) )
159 153 154 155 158 elrabf 
 |-  ( j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } <-> ( j e. ( 1 ... K ) /\ ( X ` j ) =/= ( Y ` j ) ) )
160 159 notbii 
 |-  ( -. j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } <-> -. ( j e. ( 1 ... K ) /\ ( X ` j ) =/= ( Y ` j ) ) )
161 ianor 
 |-  ( -. ( j e. ( 1 ... K ) /\ ( X ` j ) =/= ( Y ` j ) ) <-> ( -. j e. ( 1 ... K ) \/ -. ( X ` j ) =/= ( Y ` j ) ) )
162 160 161 bitri 
 |-  ( -. j e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } <-> ( -. j e. ( 1 ... K ) \/ -. ( X ` j ) =/= ( Y ` j ) ) )
163 152 162 sylib 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> ( -. j e. ( 1 ... K ) \/ -. ( X ` j ) =/= ( Y ` j ) ) )
164 imor 
 |-  ( ( j e. ( 1 ... K ) -> -. ( X ` j ) =/= ( Y ` j ) ) <-> ( -. j e. ( 1 ... K ) \/ -. ( X ` j ) =/= ( Y ` j ) ) )
165 163 164 sylibr 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> ( j e. ( 1 ... K ) -> -. ( X ` j ) =/= ( Y ` j ) ) )
166 165 imp 
 |-  ( ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) /\ j e. ( 1 ... K ) ) -> -. ( X ` j ) =/= ( Y ` j ) )
167 nne 
 |-  ( -. ( X ` j ) =/= ( Y ` j ) <-> ( X ` j ) = ( Y ` j ) )
168 166 167 sylib 
 |-  ( ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) /\ j e. ( 1 ... K ) ) -> ( X ` j ) = ( Y ` j ) )
169 134 168 mpdan 
 |-  ( ( ph /\ j e. ( 1 ... K ) /\ j < I ) -> ( X ` j ) = ( Y ` j ) )
170 169 3expa 
 |-  ( ( ( ph /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( X ` j ) = ( Y ` j ) )
171 170 3adantl2 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( X ` j ) = ( Y ` j ) )
172 171 eqcomd 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( Y ` j ) = ( X ` j ) )
173 172 breq1d 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( ( Y ` j ) < ( X ` I ) <-> ( X ` j ) < ( X ` I ) ) )
174 133 173 mpbird 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( Y ` j ) < ( X ` I ) )
175 115 174 ltned 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( Y ` j ) =/= ( X ` I ) )
176 77 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> ( X ` I ) =/= ( Y ` I ) )
177 176 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( X ` I ) =/= ( Y ` I ) )
178 177 necomd 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( Y ` I ) =/= ( X ` I ) )
179 fveq2 
 |-  ( j = I -> ( Y ` j ) = ( Y ` I ) )
180 179 neeq1d 
 |-  ( j = I -> ( ( Y ` j ) =/= ( X ` I ) <-> ( Y ` I ) =/= ( X ` I ) ) )
181 180 adantl 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( ( Y ` j ) =/= ( X ` I ) <-> ( Y ` I ) =/= ( X ` I ) ) )
182 178 181 mpbird 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( Y ` j ) =/= ( X ` I ) )
183 88 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> ( X ` I ) e. RR )
184 183 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` I ) e. RR )
185 90 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> ( Y ` I ) e. RR )
186 185 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` I ) e. RR )
187 114 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` j ) e. RR )
188 simpl2 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` I ) < ( Y ` I ) )
189 43 simprd 
 |-  ( ph -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) )
190 189 3ad2ant1 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) )
191 190 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) )
192 120 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> I e. ( 1 ... K ) )
193 108 adantr 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> j e. ( 1 ... K ) )
194 breq1 
 |-  ( x = I -> ( x < y <-> I < y ) )
195 fveq2 
 |-  ( x = I -> ( Y ` x ) = ( Y ` I ) )
196 195 breq1d 
 |-  ( x = I -> ( ( Y ` x ) < ( Y ` y ) <-> ( Y ` I ) < ( Y ` y ) ) )
197 194 196 imbi12d 
 |-  ( x = I -> ( ( x < y -> ( Y ` x ) < ( Y ` y ) ) <-> ( I < y -> ( Y ` I ) < ( Y ` y ) ) ) )
198 breq2 
 |-  ( y = j -> ( I < y <-> I < j ) )
199 fveq2 
 |-  ( y = j -> ( Y ` y ) = ( Y ` j ) )
200 199 breq2d 
 |-  ( y = j -> ( ( Y ` I ) < ( Y ` y ) <-> ( Y ` I ) < ( Y ` j ) ) )
201 198 200 imbi12d 
 |-  ( y = j -> ( ( I < y -> ( Y ` I ) < ( Y ` y ) ) <-> ( I < j -> ( Y ` I ) < ( Y ` j ) ) ) )
202 197 201 rspc2v 
 |-  ( ( I e. ( 1 ... K ) /\ j e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) -> ( I < j -> ( Y ` I ) < ( Y ` j ) ) ) )
203 192 193 202 syl2anc 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) -> ( I < j -> ( Y ` I ) < ( Y ` j ) ) ) )
204 191 203 mpd 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( I < j -> ( Y ` I ) < ( Y ` j ) ) )
205 204 syldbl2 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` I ) < ( Y ` j ) )
206 184 186 187 188 205 lttrd 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` I ) < ( Y ` j ) )
207 184 206 ltned 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` I ) =/= ( Y ` j ) )
208 207 necomd 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` j ) =/= ( X ` I ) )
209 175 182 208 3jaodan 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) /\ ( j < I \/ j = I \/ I < j ) ) -> ( Y ` j ) =/= ( X ` I ) )
210 106 209 mpdan 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) /\ j e. ( 1 ... K ) ) -> ( Y ` j ) =/= ( X ` I ) )
211 210 3expa 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) ) /\ j e. ( 1 ... K ) ) -> ( Y ` j ) =/= ( X ` I ) )
212 211 neneqd 
 |-  ( ( ( ph /\ ( X ` I ) < ( Y ` I ) ) /\ j e. ( 1 ... K ) ) -> -. ( Y ` j ) = ( X ` I ) )
213 212 ralrimiva 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) ) -> A. j e. ( 1 ... K ) -. ( Y ` j ) = ( X ` I ) )
214 ralnex 
 |-  ( A. j e. ( 1 ... K ) -. ( Y ` j ) = ( X ` I ) <-> -. E. j e. ( 1 ... K ) ( Y ` j ) = ( X ` I ) )
215 214 a1i 
 |-  ( ph -> ( A. j e. ( 1 ... K ) -. ( Y ` j ) = ( X ` I ) <-> -. E. j e. ( 1 ... K ) ( Y ` j ) = ( X ` I ) ) )
216 nnel 
 |-  ( -. ( X ` I ) e/ ran Y <-> ( X ` I ) e. ran Y )
217 216 a1i 
 |-  ( ph -> ( -. ( X ` I ) e/ ran Y <-> ( X ` I ) e. ran Y ) )
218 fvelrnb 
 |-  ( Y Fn ( 1 ... K ) -> ( ( X ` I ) e. ran Y <-> E. j e. ( 1 ... K ) ( Y ` j ) = ( X ` I ) ) )
219 47 218 syl 
 |-  ( ph -> ( ( X ` I ) e. ran Y <-> E. j e. ( 1 ... K ) ( Y ` j ) = ( X ` I ) ) )
220 217 219 bitrd 
 |-  ( ph -> ( -. ( X ` I ) e/ ran Y <-> E. j e. ( 1 ... K ) ( Y ` j ) = ( X ` I ) ) )
221 220 con1bid 
 |-  ( ph -> ( -. E. j e. ( 1 ... K ) ( Y ` j ) = ( X ` I ) <-> ( X ` I ) e/ ran Y ) )
222 215 221 bitrd 
 |-  ( ph -> ( A. j e. ( 1 ... K ) -. ( Y ` j ) = ( X ` I ) <-> ( X ` I ) e/ ran Y ) )
223 222 adantr 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) ) -> ( A. j e. ( 1 ... K ) -. ( Y ` j ) = ( X ` I ) <-> ( X ` I ) e/ ran Y ) )
224 213 223 mpbid 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) ) -> ( X ` I ) e/ ran Y )
225 elnelne1 
 |-  ( ( ( X ` I ) e. ran X /\ ( X ` I ) e/ ran Y ) -> ran X =/= ran Y )
226 100 224 225 syl2anc 
 |-  ( ( ph /\ ( X ` I ) < ( Y ` I ) ) -> ran X =/= ran Y )
227 46 ffund 
 |-  ( ph -> Fun Y )
228 227 adantr 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) ) -> Fun Y )
229 46 fdmd 
 |-  ( ph -> dom Y = ( 1 ... K ) )
230 71 229 eleqtrrd 
 |-  ( ph -> I e. dom Y )
231 230 adantr 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) ) -> I e. dom Y )
232 fvelrn 
 |-  ( ( Fun Y /\ I e. dom Y ) -> ( Y ` I ) e. ran Y )
233 228 231 232 syl2anc 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) ) -> ( Y ` I ) e. ran Y )
234 101 3ad2ant3 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> j e. NN )
235 234 nnred 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> j e. RR )
236 104 3ad2ant1 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> I e. RR )
237 235 236 lttri4d 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> ( j < I \/ j = I \/ I < j ) )
238 33 3ad2ant1 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> X : ( 1 ... K ) --> ( 1 ... N ) )
239 simp3 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> j e. ( 1 ... K ) )
240 238 239 ffvelcdmd 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> ( X ` j ) e. ( 1 ... N ) )
241 110 sseli 
 |-  ( ( X ` j ) e. ( 1 ... N ) -> ( X ` j ) e. NN )
242 240 241 syl 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> ( X ` j ) e. NN )
243 242 nnred 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> ( X ` j ) e. RR )
244 243 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( X ` j ) e. RR )
245 189 3ad2ant1 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) )
246 245 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) )
247 simpl3 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> j e. ( 1 ... K ) )
248 71 3ad2ant1 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> I e. ( 1 ... K ) )
249 248 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> I e. ( 1 ... K ) )
250 fveq2 
 |-  ( x = j -> ( Y ` x ) = ( Y ` j ) )
251 250 breq1d 
 |-  ( x = j -> ( ( Y ` x ) < ( Y ` y ) <-> ( Y ` j ) < ( Y ` y ) ) )
252 122 251 imbi12d 
 |-  ( x = j -> ( ( x < y -> ( Y ` x ) < ( Y ` y ) ) <-> ( j < y -> ( Y ` j ) < ( Y ` y ) ) ) )
253 fveq2 
 |-  ( y = I -> ( Y ` y ) = ( Y ` I ) )
254 253 breq2d 
 |-  ( y = I -> ( ( Y ` j ) < ( Y ` y ) <-> ( Y ` j ) < ( Y ` I ) ) )
255 126 254 imbi12d 
 |-  ( y = I -> ( ( j < y -> ( Y ` j ) < ( Y ` y ) ) <-> ( j < I -> ( Y ` j ) < ( Y ` I ) ) ) )
256 252 255 rspc2v 
 |-  ( ( j e. ( 1 ... K ) /\ I e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) -> ( j < I -> ( Y ` j ) < ( Y ` I ) ) ) )
257 247 249 256 syl2anc 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( Y ` x ) < ( Y ` y ) ) -> ( j < I -> ( Y ` j ) < ( Y ` I ) ) ) )
258 246 257 mpd 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( j < I -> ( Y ` j ) < ( Y ` I ) ) )
259 258 syldbl2 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( Y ` j ) < ( Y ` I ) )
260 170 3adantl2 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( X ` j ) = ( Y ` j ) )
261 260 breq1d 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( ( X ` j ) < ( Y ` I ) <-> ( Y ` j ) < ( Y ` I ) ) )
262 259 261 mpbird 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( X ` j ) < ( Y ` I ) )
263 244 262 ltned 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j < I ) -> ( X ` j ) =/= ( Y ` I ) )
264 90 3ad2ant1 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> ( Y ` I ) e. RR )
265 264 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( Y ` I ) e. RR )
266 simpl2 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( Y ` I ) < ( X ` I ) )
267 265 266 ltned 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( Y ` I ) =/= ( X ` I ) )
268 267 necomd 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( X ` I ) =/= ( Y ` I ) )
269 fveq2 
 |-  ( j = I -> ( X ` j ) = ( X ` I ) )
270 269 neeq1d 
 |-  ( j = I -> ( ( X ` j ) =/= ( Y ` I ) <-> ( X ` I ) =/= ( Y ` I ) ) )
271 270 adantl 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( ( X ` j ) =/= ( Y ` I ) <-> ( X ` I ) =/= ( Y ` I ) ) )
272 268 271 mpbird 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ j = I ) -> ( X ` j ) =/= ( Y ` I ) )
273 264 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` I ) e. RR )
274 88 3ad2ant1 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> ( X ` I ) e. RR )
275 274 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` I ) e. RR )
276 243 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` j ) e. RR )
277 simpl2 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` I ) < ( X ` I ) )
278 116 3ad2ant1 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) )
279 278 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) )
280 248 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> I e. ( 1 ... K ) )
281 239 adantr 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> j e. ( 1 ... K ) )
282 fveq2 
 |-  ( x = I -> ( X ` x ) = ( X ` I ) )
283 282 breq1d 
 |-  ( x = I -> ( ( X ` x ) < ( X ` y ) <-> ( X ` I ) < ( X ` y ) ) )
284 194 283 imbi12d 
 |-  ( x = I -> ( ( x < y -> ( X ` x ) < ( X ` y ) ) <-> ( I < y -> ( X ` I ) < ( X ` y ) ) ) )
285 fveq2 
 |-  ( y = j -> ( X ` y ) = ( X ` j ) )
286 285 breq2d 
 |-  ( y = j -> ( ( X ` I ) < ( X ` y ) <-> ( X ` I ) < ( X ` j ) ) )
287 198 286 imbi12d 
 |-  ( y = j -> ( ( I < y -> ( X ` I ) < ( X ` y ) ) <-> ( I < j -> ( X ` I ) < ( X ` j ) ) ) )
288 284 287 rspc2v 
 |-  ( ( I e. ( 1 ... K ) /\ j e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) -> ( I < j -> ( X ` I ) < ( X ` j ) ) ) )
289 280 281 288 syl2anc 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) -> ( I < j -> ( X ` I ) < ( X ` j ) ) ) )
290 279 289 mpd 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( I < j -> ( X ` I ) < ( X ` j ) ) )
291 290 syldbl2 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` I ) < ( X ` j ) )
292 273 275 276 277 291 lttrd 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` I ) < ( X ` j ) )
293 273 292 ltned 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( Y ` I ) =/= ( X ` j ) )
294 293 necomd 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ I < j ) -> ( X ` j ) =/= ( Y ` I ) )
295 263 272 294 3jaodan 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) /\ ( j < I \/ j = I \/ I < j ) ) -> ( X ` j ) =/= ( Y ` I ) )
296 237 295 mpdan 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) /\ j e. ( 1 ... K ) ) -> ( X ` j ) =/= ( Y ` I ) )
297 296 3expa 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) ) /\ j e. ( 1 ... K ) ) -> ( X ` j ) =/= ( Y ` I ) )
298 297 neneqd 
 |-  ( ( ( ph /\ ( Y ` I ) < ( X ` I ) ) /\ j e. ( 1 ... K ) ) -> -. ( X ` j ) = ( Y ` I ) )
299 298 ralrimiva 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) ) -> A. j e. ( 1 ... K ) -. ( X ` j ) = ( Y ` I ) )
300 ralnex 
 |-  ( A. j e. ( 1 ... K ) -. ( X ` j ) = ( Y ` I ) <-> -. E. j e. ( 1 ... K ) ( X ` j ) = ( Y ` I ) )
301 300 a1i 
 |-  ( ph -> ( A. j e. ( 1 ... K ) -. ( X ` j ) = ( Y ` I ) <-> -. E. j e. ( 1 ... K ) ( X ` j ) = ( Y ` I ) ) )
302 nnel 
 |-  ( -. ( Y ` I ) e/ ran X <-> ( Y ` I ) e. ran X )
303 302 a1i 
 |-  ( ph -> ( -. ( Y ` I ) e/ ran X <-> ( Y ` I ) e. ran X ) )
304 fvelrnb 
 |-  ( X Fn ( 1 ... K ) -> ( ( Y ` I ) e. ran X <-> E. j e. ( 1 ... K ) ( X ` j ) = ( Y ` I ) ) )
305 34 304 syl 
 |-  ( ph -> ( ( Y ` I ) e. ran X <-> E. j e. ( 1 ... K ) ( X ` j ) = ( Y ` I ) ) )
306 303 305 bitrd 
 |-  ( ph -> ( -. ( Y ` I ) e/ ran X <-> E. j e. ( 1 ... K ) ( X ` j ) = ( Y ` I ) ) )
307 306 con1bid 
 |-  ( ph -> ( -. E. j e. ( 1 ... K ) ( X ` j ) = ( Y ` I ) <-> ( Y ` I ) e/ ran X ) )
308 301 307 bitrd 
 |-  ( ph -> ( A. j e. ( 1 ... K ) -. ( X ` j ) = ( Y ` I ) <-> ( Y ` I ) e/ ran X ) )
309 308 adantr 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) ) -> ( A. j e. ( 1 ... K ) -. ( X ` j ) = ( Y ` I ) <-> ( Y ` I ) e/ ran X ) )
310 299 309 mpbid 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) ) -> ( Y ` I ) e/ ran X )
311 elnelne1 
 |-  ( ( ( Y ` I ) e. ran Y /\ ( Y ` I ) e/ ran X ) -> ran Y =/= ran X )
312 311 necomd 
 |-  ( ( ( Y ` I ) e. ran Y /\ ( Y ` I ) e/ ran X ) -> ran X =/= ran Y )
313 233 310 312 syl2anc 
 |-  ( ( ph /\ ( Y ` I ) < ( X ` I ) ) -> ran X =/= ran Y )
314 226 313 jaodan 
 |-  ( ( ph /\ ( ( X ` I ) < ( Y ` I ) \/ ( Y ` I ) < ( X ` I ) ) ) -> ran X =/= ran Y )
315 93 314 mpdan 
 |-  ( ph -> ran X =/= ran Y )