Metamath Proof Explorer

Theorem sticksstones3

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

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

Proof

Step Hyp Ref Expression
1 sticksstones3.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones3.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones3.3 
 |-  B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K }
4 sticksstones3.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 sticksstones3.5 
 |-  F = ( z e. A |-> ran z )
6 1 2 3 4 5 sticksstones2 
 |-  ( ph -> F : A -1-1-> B )
7 df-f1 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
8 7 biimpi 
 |-  ( F : A -1-1-> B -> ( F : A --> B /\ Fun `' F ) )
9 8 simpld 
 |-  ( F : A -1-1-> B -> F : A --> B )
10 6 9 syl 
 |-  ( ph -> F : A --> B )
11 3 eleq2i 
 |-  ( w e. B <-> w e. { a e. ~P ( 1 ... N ) | ( # ` a ) = K } )
12 11 bilani 
 |-  ( ( ph /\ w e. B ) -> w e. { a e. ~P ( 1 ... N ) | ( # ` a ) = K } )
13 fveqeq2 
 |-  ( a = w -> ( ( # ` a ) = K <-> ( # ` w ) = K ) )
14 13 elrab 
 |-  ( w e. { a e. ~P ( 1 ... N ) | ( # ` a ) = K } <-> ( w e. ~P ( 1 ... N ) /\ ( # ` w ) = K ) )
15 12 14 sylib 
 |-  ( ( ph /\ w e. B ) -> ( w e. ~P ( 1 ... N ) /\ ( # ` w ) = K ) )
16 15 simpld 
 |-  ( ( ph /\ w e. B ) -> w e. ~P ( 1 ... N ) )
17 16 elpwid 
 |-  ( ( ph /\ w e. B ) -> w C_ ( 1 ... N ) )
18 17 sseld 
 |-  ( ( ph /\ w e. B ) -> ( c e. w -> c e. ( 1 ... N ) ) )
19 18 imp 
 |-  ( ( ( ph /\ w e. B ) /\ c e. w ) -> c e. ( 1 ... N ) )
20 19 3impa 
 |-  ( ( ph /\ w e. B /\ c e. w ) -> c e. ( 1 ... N ) )
21 elfznn 
 |-  ( c e. ( 1 ... N ) -> c e. NN )
22 20 21 syl 
 |-  ( ( ph /\ w e. B /\ c e. w ) -> c e. NN )
23 22 nnred 
 |-  ( ( ph /\ w e. B /\ c e. w ) -> c e. RR )
24 23 3expa 
 |-  ( ( ( ph /\ w e. B ) /\ c e. w ) -> c e. RR )
25 24 ex 
 |-  ( ( ph /\ w e. B ) -> ( c e. w -> c e. RR ) )
26 25 ssrdv 
 |-  ( ( ph /\ w e. B ) -> w C_ RR )
27 ltso 
 |-  < Or RR
28 soss 
 |-  ( w C_ RR -> ( < Or RR -> < Or w ) )
29 27 28 mpi 
 |-  ( w C_ RR -> < Or w )
30 26 29 syl 
 |-  ( ( ph /\ w e. B ) -> < Or w )
31 fzfid 
 |-  ( ( ph /\ w e. B ) -> ( 1 ... N ) e. Fin )
32 31 17 ssfid 
 |-  ( ( ph /\ w e. B ) -> w e. Fin )
33 fz1iso 
 |-  ( ( < Or w /\ w e. Fin ) -> E. v v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) )
34 30 32 33 syl2anc 
 |-  ( ( ph /\ w e. B ) -> E. v v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) )
35 df-isom 
 |-  ( v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) <-> ( v : ( 1 ... ( # ` w ) ) -1-1-onto-> w /\ A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y <-> ( v ` x ) < ( v ` y ) ) ) )
36 35 biimpi 
 |-  ( v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) -> ( v : ( 1 ... ( # ` w ) ) -1-1-onto-> w /\ A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y <-> ( v ` x ) < ( v ` y ) ) ) )
37 36 3ad2ant3 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( v : ( 1 ... ( # ` w ) ) -1-1-onto-> w /\ A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y <-> ( v ` x ) < ( v ` y ) ) ) )
38 37 simpld 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v : ( 1 ... ( # ` w ) ) -1-1-onto-> w )
39 15 simprd 
 |-  ( ( ph /\ w e. B ) -> ( # ` w ) = K )
40 oveq2 
 |-  ( ( # ` w ) = K -> ( 1 ... ( # ` w ) ) = ( 1 ... K ) )
41 40 f1oeq2d 
 |-  ( ( # ` w ) = K -> ( v : ( 1 ... ( # ` w ) ) -1-1-onto-> w <-> v : ( 1 ... K ) -1-1-onto-> w ) )
42 39 41 syl 
 |-  ( ( ph /\ w e. B ) -> ( v : ( 1 ... ( # ` w ) ) -1-1-onto-> w <-> v : ( 1 ... K ) -1-1-onto-> w ) )
43 42 biimpd 
 |-  ( ( ph /\ w e. B ) -> ( v : ( 1 ... ( # ` w ) ) -1-1-onto-> w -> v : ( 1 ... K ) -1-1-onto-> w ) )
44 43 3adant3 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( v : ( 1 ... ( # ` w ) ) -1-1-onto-> w -> v : ( 1 ... K ) -1-1-onto-> w ) )
45 38 44 mpd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v : ( 1 ... K ) -1-1-onto-> w )
46 f1of 
 |-  ( v : ( 1 ... K ) -1-1-onto-> w -> v : ( 1 ... K ) --> w )
47 45 46 syl 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v : ( 1 ... K ) --> w )
48 47 ffnd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v Fn ( 1 ... K ) )
49 ovexd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( 1 ... K ) e. _V )
50 48 49 fnexd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v e. _V )
51 17 3adant3 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> w C_ ( 1 ... N ) )
52 fss 
 |-  ( ( v : ( 1 ... K ) --> w /\ w C_ ( 1 ... N ) ) -> v : ( 1 ... K ) --> ( 1 ... N ) )
53 47 51 52 syl2anc 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v : ( 1 ... K ) --> ( 1 ... N ) )
54 37 simprd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y <-> ( v ` x ) < ( v ` y ) ) )
55 biimp 
 |-  ( ( x < y <-> ( v ` x ) < ( v ` y ) ) -> ( x < y -> ( v ` x ) < ( v ` y ) ) )
56 55 a1i 
 |-  ( ( ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) /\ x e. ( 1 ... ( # ` w ) ) ) /\ y e. ( 1 ... ( # ` w ) ) ) -> ( ( x < y <-> ( v ` x ) < ( v ` y ) ) -> ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
57 56 ralimdva 
 |-  ( ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) /\ x e. ( 1 ... ( # ` w ) ) ) -> ( A. y e. ( 1 ... ( # ` w ) ) ( x < y <-> ( v ` x ) < ( v ` y ) ) -> A. y e. ( 1 ... ( # ` w ) ) ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
58 57 ralimdva 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y <-> ( v ` x ) < ( v ` y ) ) -> A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
59 54 58 mpd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y -> ( v ` x ) < ( v ` y ) ) )
60 39 adantr 
 |-  ( ( ( ph /\ w e. B ) /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( # ` w ) = K )
61 60 3impa 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( # ` w ) = K )
62 61 oveq2d 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( 1 ... ( # ` w ) ) = ( 1 ... K ) )
63 62 raleqdv 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( A. y e. ( 1 ... ( # ` w ) ) ( x < y -> ( v ` x ) < ( v ` y ) ) <-> A. y e. ( 1 ... K ) ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
64 63 adantr 
 |-  ( ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) /\ x e. ( 1 ... ( # ` w ) ) ) -> ( A. y e. ( 1 ... ( # ` w ) ) ( x < y -> ( v ` x ) < ( v ` y ) ) <-> A. y e. ( 1 ... K ) ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
65 62 64 raleqbidva 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( A. x e. ( 1 ... ( # ` w ) ) A. y e. ( 1 ... ( # ` w ) ) ( x < y -> ( v ` x ) < ( v ` y ) ) <-> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
66 59 65 mpbid 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( v ` x ) < ( v ` y ) ) )
67 53 66 jca 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( v : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
68 feq1 
 |-  ( f = v -> ( f : ( 1 ... K ) --> ( 1 ... N ) <-> v : ( 1 ... K ) --> ( 1 ... N ) ) )
69 fveq1 
 |-  ( f = v -> ( f ` x ) = ( v ` x ) )
70 fveq1 
 |-  ( f = v -> ( f ` y ) = ( v ` y ) )
71 69 70 breq12d 
 |-  ( f = v -> ( ( f ` x ) < ( f ` y ) <-> ( v ` x ) < ( v ` y ) ) )
72 71 imbi2d 
 |-  ( f = v -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( v ` x ) < ( v ` y ) ) ) )
73 72 2ralbidv 
 |-  ( f = v -> ( 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 -> ( v ` x ) < ( v ` y ) ) ) )
74 68 73 anbi12d 
 |-  ( f = v -> ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( v : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( v ` x ) < ( v ` y ) ) ) ) )
75 50 67 74 elabd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v e. { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
76 4 eleq2i 
 |-  ( v e. A <-> v e. { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
77 75 76 sylibr 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> v e. A )
78 5 a1i 
 |-  ( ( ph /\ v e. A ) -> F = ( z e. A |-> ran z ) )
79 simpr 
 |-  ( ( ( ph /\ v e. A ) /\ z = v ) -> z = v )
80 79 rneqd 
 |-  ( ( ( ph /\ v e. A ) /\ z = v ) -> ran z = ran v )
81 simpr 
 |-  ( ( ph /\ v e. A ) -> v e. A )
82 rnexg 
 |-  ( v e. A -> ran v e. _V )
83 81 82 syl 
 |-  ( ( ph /\ v e. A ) -> ran v e. _V )
84 78 80 81 83 fvmptd 
 |-  ( ( ph /\ v e. A ) -> ( F ` v ) = ran v )
85 84 ex 
 |-  ( ph -> ( v e. A -> ( F ` v ) = ran v ) )
86 85 3ad2ant1 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( v e. A -> ( F ` v ) = ran v ) )
87 77 86 mpd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( F ` v ) = ran v )
88 dff1o2 
 |-  ( v : ( 1 ... K ) -1-1-onto-> w <-> ( v Fn ( 1 ... K ) /\ Fun `' v /\ ran v = w ) )
89 88 biimpi 
 |-  ( v : ( 1 ... K ) -1-1-onto-> w -> ( v Fn ( 1 ... K ) /\ Fun `' v /\ ran v = w ) )
90 89 simp3d 
 |-  ( v : ( 1 ... K ) -1-1-onto-> w -> ran v = w )
91 45 90 syl 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ran v = w )
92 87 91 eqtrd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( F ` v ) = w )
93 92 eqcomd 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> w = ( F ` v ) )
94 77 93 jca 
 |-  ( ( ph /\ w e. B /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( v e. A /\ w = ( F ` v ) ) )
95 94 3expa 
 |-  ( ( ( ph /\ w e. B ) /\ v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) ) -> ( v e. A /\ w = ( F ` v ) ) )
96 95 ex 
 |-  ( ( ph /\ w e. B ) -> ( v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) -> ( v e. A /\ w = ( F ` v ) ) ) )
97 96 eximdv 
 |-  ( ( ph /\ w e. B ) -> ( E. v v Isom < , < ( ( 1 ... ( # ` w ) ) , w ) -> E. v ( v e. A /\ w = ( F ` v ) ) ) )
98 34 97 mpd 
 |-  ( ( ph /\ w e. B ) -> E. v ( v e. A /\ w = ( F ` v ) ) )
99 df-rex 
 |-  ( E. v e. A w = ( F ` v ) <-> E. v ( v e. A /\ w = ( F ` v ) ) )
100 98 99 sylibr 
 |-  ( ( ph /\ w e. B ) -> E. v e. A w = ( F ` v ) )
101 100 ralrimiva 
 |-  ( ph -> A. w e. B E. v e. A w = ( F ` v ) )
102 10 101 jca 
 |-  ( ph -> ( F : A --> B /\ A. w e. B E. v e. A w = ( F ` v ) ) )
103 dffo3 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. w e. B E. v e. A w = ( F ` v ) ) )
104 103 a1i 
 |-  ( ph -> ( F : A -onto-> B <-> ( F : A --> B /\ A. w e. B E. v e. A w = ( F ` v ) ) ) )
105 102 104 mpbird 
 |-  ( ph -> F : A -onto-> B )