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 φ N 0
sticksstones3.2 φ K 0
sticksstones3.3 B = a 𝒫 1 N | a = K
sticksstones3.4 A = f | f : 1 K 1 N x 1 K y 1 K x < y f x < f y
sticksstones3.5 F = z A ran z
Assertion sticksstones3 φ F : A onto B

Proof

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