Metamath Proof Explorer

Theorem sticksstones2

Description: The range function on strictly monotone functions with finite domain and codomain is an injective mapping onto K -elemental sets. (Contributed by metakunt, 27-Sep-2024)

Ref Expression
Hypotheses sticksstones2.1 
|- ( ph -> N e. NN0 )
sticksstones2.2 
|- ( ph -> K e. NN0 )
sticksstones2.3 
|- B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K }
sticksstones2.4 
|- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
sticksstones2.5 
|- F = ( z e. A |-> ran z )
Assertion sticksstones2 
|- ( ph -> F : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 sticksstones2.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones2.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones2.3 
 |-  B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K }
4 sticksstones2.4 
 |-  A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
5 sticksstones2.5 
 |-  F = ( z e. A |-> ran z )
6 fveqeq2 
 |-  ( a = ran z -> ( ( # ` a ) = K <-> ( # ` ran z ) = K ) )
7 fzfid 
 |-  ( ( ph /\ z e. A ) -> ( 1 ... N ) e. Fin )
8 eleq1w 
 |-  ( f = z -> ( f e. A <-> z e. A ) )
9 feq1 
 |-  ( f = z -> ( f : ( 1 ... K ) --> ( 1 ... N ) <-> z : ( 1 ... K ) --> ( 1 ... N ) ) )
10 fveq1 
 |-  ( f = z -> ( f ` x ) = ( z ` x ) )
11 fveq1 
 |-  ( f = z -> ( f ` y ) = ( z ` y ) )
12 10 11 breq12d 
 |-  ( f = z -> ( ( f ` x ) < ( f ` y ) <-> ( z ` x ) < ( z ` y ) ) )
13 12 imbi2d 
 |-  ( f = z -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( z ` x ) < ( z ` y ) ) ) )
14 13 ralbidv 
 |-  ( f = z -> ( A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) <-> A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) ) )
15 14 ralbidv 
 |-  ( f = z -> ( 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 -> ( z ` x ) < ( z ` y ) ) ) )
16 9 15 anbi12d 
 |-  ( f = z -> ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( z : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) ) ) )
17 8 16 bibi12d 
 |-  ( f = z -> ( ( f e. A <-> ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) ) <-> ( z e. A <-> ( z : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) ) ) ) )
18 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 ) ) ) ) )
19 4 18 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 ) ) ) )
20 19 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 ) ) ) )
21 17 20 chvarvv 
 |-  ( z e. A <-> ( z : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) ) )
22 21 biimpi 
 |-  ( z e. A -> ( z : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) ) )
23 22 adantl 
 |-  ( ( ph /\ z e. A ) -> ( z : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) ) )
24 23 simpld 
 |-  ( ( ph /\ z e. A ) -> z : ( 1 ... K ) --> ( 1 ... N ) )
25 24 frnd 
 |-  ( ( ph /\ z e. A ) -> ran z C_ ( 1 ... N ) )
26 7 25 sselpwd 
 |-  ( ( ph /\ z e. A ) -> ran z e. ~P ( 1 ... N ) )
27 24 ffnd 
 |-  ( ( ph /\ z e. A ) -> z Fn ( 1 ... K ) )
28 hashfn 
 |-  ( z Fn ( 1 ... K ) -> ( # ` z ) = ( # ` ( 1 ... K ) ) )
29 27 28 syl 
 |-  ( ( ph /\ z e. A ) -> ( # ` z ) = ( # ` ( 1 ... K ) ) )
30 2 adantr 
 |-  ( ( ph /\ z e. A ) -> K e. NN0 )
31 hashfz1 
 |-  ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
32 30 31 syl 
 |-  ( ( ph /\ z e. A ) -> ( # ` ( 1 ... K ) ) = K )
33 29 32 eqtrd 
 |-  ( ( ph /\ z e. A ) -> ( # ` z ) = K )
34 33 eqcomd 
 |-  ( ( ph /\ z e. A ) -> K = ( # ` z ) )
35 fzfid 
 |-  ( ( ph /\ z e. A ) -> ( 1 ... K ) e. Fin )
36 elfznn 
 |-  ( a e. ( 1 ... K ) -> a e. NN )
37 36 3ad2ant3 
 |-  ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) -> a e. NN )
38 37 nnred 
 |-  ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) -> a e. RR )
39 38 adantr 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> a e. RR )
40 elfznn 
 |-  ( b e. ( 1 ... K ) -> b e. NN )
41 40 nnred 
 |-  ( b e. ( 1 ... K ) -> b e. RR )
42 41 adantl 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> b e. RR )
43 lttri2 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a =/= b <-> ( a < b \/ b < a ) ) )
44 39 42 43 syl2anc 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( a =/= b <-> ( a < b \/ b < a ) ) )
45 24 3adant3 
 |-  ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) -> z : ( 1 ... K ) --> ( 1 ... N ) )
46 simp3 
 |-  ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) -> a e. ( 1 ... K ) )
47 45 46 ffvelrnd 
 |-  ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) -> ( z ` a ) e. ( 1 ... N ) )
48 47 adantr 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( z ` a ) e. ( 1 ... N ) )
49 48 adantr 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ a < b ) -> ( z ` a ) e. ( 1 ... N ) )
50 elfznn 
 |-  ( ( z ` a ) e. ( 1 ... N ) -> ( z ` a ) e. NN )
51 49 50 syl 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ a < b ) -> ( z ` a ) e. NN )
52 51 nnred 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ a < b ) -> ( z ` a ) e. RR )
53 23 simprd 
 |-  ( ( ph /\ z e. A ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) )
54 53 3adant3 
 |-  ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) )
55 54 adantr 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) )
56 46 adantr 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> a e. ( 1 ... K ) )
57 simpr 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> b e. ( 1 ... K ) )
58 breq1 
 |-  ( x = a -> ( x < y <-> a < y ) )
59 fveq2 
 |-  ( x = a -> ( z ` x ) = ( z ` a ) )
60 59 breq1d 
 |-  ( x = a -> ( ( z ` x ) < ( z ` y ) <-> ( z ` a ) < ( z ` y ) ) )
61 58 60 imbi12d 
 |-  ( x = a -> ( ( x < y -> ( z ` x ) < ( z ` y ) ) <-> ( a < y -> ( z ` a ) < ( z ` y ) ) ) )
62 breq2 
 |-  ( y = b -> ( a < y <-> a < b ) )
63 fveq2 
 |-  ( y = b -> ( z ` y ) = ( z ` b ) )
64 63 breq2d 
 |-  ( y = b -> ( ( z ` a ) < ( z ` y ) <-> ( z ` a ) < ( z ` b ) ) )
65 62 64 imbi12d 
 |-  ( y = b -> ( ( a < y -> ( z ` a ) < ( z ` y ) ) <-> ( a < b -> ( z ` a ) < ( z ` b ) ) ) )
66 61 65 rspc2v 
 |-  ( ( a e. ( 1 ... K ) /\ b e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) -> ( a < b -> ( z ` a ) < ( z ` b ) ) ) )
67 56 57 66 syl2anc 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) -> ( a < b -> ( z ` a ) < ( z ` b ) ) ) )
68 55 67 mpd 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( a < b -> ( z ` a ) < ( z ` b ) ) )
69 68 imp 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ a < b ) -> ( z ` a ) < ( z ` b ) )
70 52 69 ltned 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ a < b ) -> ( z ` a ) =/= ( z ` b ) )
71 45 ffvelrnda 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( z ` b ) e. ( 1 ... N ) )
72 elfznn 
 |-  ( ( z ` b ) e. ( 1 ... N ) -> ( z ` b ) e. NN )
73 71 72 syl 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( z ` b ) e. NN )
74 73 nnred 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( z ` b ) e. RR )
75 74 adantr 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ b < a ) -> ( z ` b ) e. RR )
76 breq1 
 |-  ( x = b -> ( x < y <-> b < y ) )
77 fveq2 
 |-  ( x = b -> ( z ` x ) = ( z ` b ) )
78 77 breq1d 
 |-  ( x = b -> ( ( z ` x ) < ( z ` y ) <-> ( z ` b ) < ( z ` y ) ) )
79 76 78 imbi12d 
 |-  ( x = b -> ( ( x < y -> ( z ` x ) < ( z ` y ) ) <-> ( b < y -> ( z ` b ) < ( z ` y ) ) ) )
80 breq2 
 |-  ( y = a -> ( b < y <-> b < a ) )
81 fveq2 
 |-  ( y = a -> ( z ` y ) = ( z ` a ) )
82 81 breq2d 
 |-  ( y = a -> ( ( z ` b ) < ( z ` y ) <-> ( z ` b ) < ( z ` a ) ) )
83 80 82 imbi12d 
 |-  ( y = a -> ( ( b < y -> ( z ` b ) < ( z ` y ) ) <-> ( b < a -> ( z ` b ) < ( z ` a ) ) ) )
84 79 83 rspc2v 
 |-  ( ( b e. ( 1 ... K ) /\ a e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) -> ( b < a -> ( z ` b ) < ( z ` a ) ) ) )
85 57 56 84 syl2anc 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( z ` x ) < ( z ` y ) ) -> ( b < a -> ( z ` b ) < ( z ` a ) ) ) )
86 55 85 mpd 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( b < a -> ( z ` b ) < ( z ` a ) ) )
87 86 imp 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ b < a ) -> ( z ` b ) < ( z ` a ) )
88 75 87 ltned 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ b < a ) -> ( z ` b ) =/= ( z ` a ) )
89 88 necomd 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ b < a ) -> ( z ` a ) =/= ( z ` b ) )
90 70 89 jaodan 
 |-  ( ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) /\ ( a < b \/ b < a ) ) -> ( z ` a ) =/= ( z ` b ) )
91 90 ex 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( ( a < b \/ b < a ) -> ( z ` a ) =/= ( z ` b ) ) )
92 44 91 sylbid 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( a =/= b -> ( z ` a ) =/= ( z ` b ) ) )
93 92 necon4d 
 |-  ( ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) /\ b e. ( 1 ... K ) ) -> ( ( z ` a ) = ( z ` b ) -> a = b ) )
94 93 ralrimiva 
 |-  ( ( ph /\ z e. A /\ a e. ( 1 ... K ) ) -> A. b e. ( 1 ... K ) ( ( z ` a ) = ( z ` b ) -> a = b ) )
95 94 3expa 
 |-  ( ( ( ph /\ z e. A ) /\ a e. ( 1 ... K ) ) -> A. b e. ( 1 ... K ) ( ( z ` a ) = ( z ` b ) -> a = b ) )
96 95 ralrimiva 
 |-  ( ( ph /\ z e. A ) -> A. a e. ( 1 ... K ) A. b e. ( 1 ... K ) ( ( z ` a ) = ( z ` b ) -> a = b ) )
97 24 96 jca 
 |-  ( ( ph /\ z e. A ) -> ( z : ( 1 ... K ) --> ( 1 ... N ) /\ A. a e. ( 1 ... K ) A. b e. ( 1 ... K ) ( ( z ` a ) = ( z ` b ) -> a = b ) ) )
98 dff13 
 |-  ( z : ( 1 ... K ) -1-1-> ( 1 ... N ) <-> ( z : ( 1 ... K ) --> ( 1 ... N ) /\ A. a e. ( 1 ... K ) A. b e. ( 1 ... K ) ( ( z ` a ) = ( z ` b ) -> a = b ) ) )
99 97 98 sylibr 
 |-  ( ( ph /\ z e. A ) -> z : ( 1 ... K ) -1-1-> ( 1 ... N ) )
100 hashf1rn 
 |-  ( ( ( 1 ... K ) e. Fin /\ z : ( 1 ... K ) -1-1-> ( 1 ... N ) ) -> ( # ` z ) = ( # ` ran z ) )
101 35 99 100 syl2anc 
 |-  ( ( ph /\ z e. A ) -> ( # ` z ) = ( # ` ran z ) )
102 34 101 eqtrd 
 |-  ( ( ph /\ z e. A ) -> K = ( # ` ran z ) )
103 102 eqcomd 
 |-  ( ( ph /\ z e. A ) -> ( # ` ran z ) = K )
104 6 26 103 elrabd 
 |-  ( ( ph /\ z e. A ) -> ran z e. { a e. ~P ( 1 ... N ) | ( # ` a ) = K } )
105 3 eleq2i 
 |-  ( ran z e. B <-> ran z e. { a e. ~P ( 1 ... N ) | ( # ` a ) = K } )
106 105 a1i 
 |-  ( ( ph /\ z e. A ) -> ( ran z e. B <-> ran z e. { a e. ~P ( 1 ... N ) | ( # ` a ) = K } ) )
107 104 106 mpbird 
 |-  ( ( ph /\ z e. A ) -> ran z e. B )
108 107 5 fmptd 
 |-  ( ph -> F : A --> B )
109 1 3ad2ant1 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> N e. NN0 )
110 109 adantr 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> N e. NN0 )
111 2 3ad2ant1 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> K e. NN0 )
112 111 adantr 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> K e. NN0 )
113 simpl2 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> i e. A )
114 simpl3 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> j e. A )
115 simpr 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> i =/= j )
116 fveq2 
 |-  ( r = s -> ( i ` r ) = ( i ` s ) )
117 fveq2 
 |-  ( r = s -> ( j ` r ) = ( j ` s ) )
118 116 117 neeq12d 
 |-  ( r = s -> ( ( i ` r ) =/= ( j ` r ) <-> ( i ` s ) =/= ( j ` s ) ) )
119 118 cbvrabv 
 |-  { r e. ( 1 ... K ) | ( i ` r ) =/= ( j ` r ) } = { s e. ( 1 ... K ) | ( i ` s ) =/= ( j ` s ) }
120 119 infeq1i 
 |-  inf ( { r e. ( 1 ... K ) | ( i ` r ) =/= ( j ` r ) } , RR , < ) = inf ( { s e. ( 1 ... K ) | ( i ` s ) =/= ( j ` s ) } , RR , < )
121 110 112 4 113 114 115 120 sticksstones1 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ran i =/= ran j )
122 5 a1i 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> F = ( z e. A |-> ran z ) )
123 simpr 
 |-  ( ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) /\ z = i ) -> z = i )
124 123 rneqd 
 |-  ( ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) /\ z = i ) -> ran z = ran i )
125 fzfid 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ( 1 ... N ) e. Fin )
126 eleq1w 
 |-  ( f = i -> ( f e. A <-> i e. A ) )
127 feq1 
 |-  ( f = i -> ( f : ( 1 ... K ) --> ( 1 ... N ) <-> i : ( 1 ... K ) --> ( 1 ... N ) ) )
128 fveq1 
 |-  ( f = i -> ( f ` x ) = ( i ` x ) )
129 fveq1 
 |-  ( f = i -> ( f ` y ) = ( i ` y ) )
130 128 129 breq12d 
 |-  ( f = i -> ( ( f ` x ) < ( f ` y ) <-> ( i ` x ) < ( i ` y ) ) )
131 130 imbi2d 
 |-  ( f = i -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( i ` x ) < ( i ` y ) ) ) )
132 131 2ralbidv 
 |-  ( f = i -> ( 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 -> ( i ` x ) < ( i ` y ) ) ) )
133 127 132 anbi12d 
 |-  ( f = i -> ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( i : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( i ` x ) < ( i ` y ) ) ) ) )
134 126 133 bibi12d 
 |-  ( f = i -> ( ( f e. A <-> ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) ) <-> ( i e. A <-> ( i : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( i ` x ) < ( i ` y ) ) ) ) ) )
135 134 20 chvarvv 
 |-  ( i e. A <-> ( i : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( i ` x ) < ( i ` y ) ) ) )
136 135 biimpi 
 |-  ( i e. A -> ( i : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( i ` x ) < ( i ` y ) ) ) )
137 136 adantl 
 |-  ( ( ph /\ i e. A ) -> ( i : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( i ` x ) < ( i ` y ) ) ) )
138 137 simpld 
 |-  ( ( ph /\ i e. A ) -> i : ( 1 ... K ) --> ( 1 ... N ) )
139 138 3adant3 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> i : ( 1 ... K ) --> ( 1 ... N ) )
140 139 adantr 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> i : ( 1 ... K ) --> ( 1 ... N ) )
141 140 frnd 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ran i C_ ( 1 ... N ) )
142 125 141 sselpwd 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ran i e. ~P ( 1 ... N ) )
143 122 124 113 142 fvmptd 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ( F ` i ) = ran i )
144 simpr 
 |-  ( ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) /\ z = j ) -> z = j )
145 144 rneqd 
 |-  ( ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) /\ z = j ) -> ran z = ran j )
146 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
147 146 3ad2ant1 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> ( 1 ... N ) e. Fin )
148 eleq1w 
 |-  ( f = j -> ( f e. A <-> j e. A ) )
149 feq1 
 |-  ( f = j -> ( f : ( 1 ... K ) --> ( 1 ... N ) <-> j : ( 1 ... K ) --> ( 1 ... N ) ) )
150 fveq1 
 |-  ( f = j -> ( f ` x ) = ( j ` x ) )
151 fveq1 
 |-  ( f = j -> ( f ` y ) = ( j ` y ) )
152 150 151 breq12d 
 |-  ( f = j -> ( ( f ` x ) < ( f ` y ) <-> ( j ` x ) < ( j ` y ) ) )
153 152 imbi2d 
 |-  ( f = j -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( j ` x ) < ( j ` y ) ) ) )
154 153 2ralbidv 
 |-  ( f = j -> ( 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 -> ( j ` x ) < ( j ` y ) ) ) )
155 149 154 anbi12d 
 |-  ( f = j -> ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( j : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( j ` x ) < ( j ` y ) ) ) ) )
156 148 155 bibi12d 
 |-  ( f = j -> ( ( f e. A <-> ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) ) <-> ( j e. A <-> ( j : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( j ` x ) < ( j ` y ) ) ) ) ) )
157 156 20 chvarvv 
 |-  ( j e. A <-> ( j : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( j ` x ) < ( j ` y ) ) ) )
158 157 biimpi 
 |-  ( j e. A -> ( j : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( j ` x ) < ( j ` y ) ) ) )
159 158 adantl 
 |-  ( ( ph /\ j e. A ) -> ( j : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( j ` x ) < ( j ` y ) ) ) )
160 159 simpld 
 |-  ( ( ph /\ j e. A ) -> j : ( 1 ... K ) --> ( 1 ... N ) )
161 160 3adant2 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> j : ( 1 ... K ) --> ( 1 ... N ) )
162 161 frnd 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> ran j C_ ( 1 ... N ) )
163 147 162 sselpwd 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> ran j e. ~P ( 1 ... N ) )
164 163 adantr 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ran j e. ~P ( 1 ... N ) )
165 122 145 114 164 fvmptd 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ( F ` j ) = ran j )
166 121 143 165 3netr4d 
 |-  ( ( ( ph /\ i e. A /\ j e. A ) /\ i =/= j ) -> ( F ` i ) =/= ( F ` j ) )
167 166 ex 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> ( i =/= j -> ( F ` i ) =/= ( F ` j ) ) )
168 167 necon4d 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> ( ( F ` i ) = ( F ` j ) -> i = j ) )
169 168 3expa 
 |-  ( ( ( ph /\ i e. A ) /\ j e. A ) -> ( ( F ` i ) = ( F ` j ) -> i = j ) )
170 169 ralrimiva 
 |-  ( ( ph /\ i e. A ) -> A. j e. A ( ( F ` i ) = ( F ` j ) -> i = j ) )
171 170 ralrimiva 
 |-  ( ph -> A. i e. A A. j e. A ( ( F ` i ) = ( F ` j ) -> i = j ) )
172 108 171 jca 
 |-  ( ph -> ( F : A --> B /\ A. i e. A A. j e. A ( ( F ` i ) = ( F ` j ) -> i = j ) ) )
173 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. i e. A A. j e. A ( ( F ` i ) = ( F ` j ) -> i = j ) ) )
174 172 173 sylibr 
 |-  ( ph -> F : A -1-1-> B )