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