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