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