Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wessf1ornlem Structured version   Visualization version   Unicode version

Theorem wessf1ornlem 37530
 Description: Given a function on a well ordered domain there exists a subset of such that restricted to such subset is injective and onto the range of (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
wessf1ornlem.f
wessf1ornlem.a
wessf1ornlem.r
wessf1ornlem.g
Assertion
Ref Expression
wessf1ornlem
Distinct variable groups:   ,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,)   (,,)   (,,)

Proof of Theorem wessf1ornlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvimass 5194 . . . . . . . . 9
21a1i 11 . . . . . . . 8
3 wessf1ornlem.f . . . . . . . . . 10
4 fndm 5685 . . . . . . . . . 10
53, 4syl 17 . . . . . . . . 9
65adantr 472 . . . . . . . 8
72, 6sseqtrd 3454 . . . . . . 7
8 wessf1ornlem.r . . . . . . . . . 10
98adantr 472 . . . . . . . . 9
101, 5syl5sseq 3466 . . . . . . . . . . 11
11 wessf1ornlem.a . . . . . . . . . . 11
12 ssexg 4542 . . . . . . . . . . 11
1310, 11, 12syl2anc 673 . . . . . . . . . 10
1413adantr 472 . . . . . . . . 9
15 inisegn0 5206 . . . . . . . . . . 11
1615biimpi 199 . . . . . . . . . 10
1716adantl 473 . . . . . . . . 9
18 wereu 4835 . . . . . . . . 9
199, 14, 7, 17, 18syl13anc 1294 . . . . . . . 8
20 riotacl 6284 . . . . . . . 8
2119, 20syl 17 . . . . . . 7
227, 21sseldd 3419 . . . . . 6
2322ralrimiva 2809 . . . . 5
24 wessf1ornlem.g . . . . . . 7
25 sneq 3969 . . . . . . . . . . 11
2625imaeq2d 5174 . . . . . . . . . 10
2726raleqdv 2979 . . . . . . . . . 10
2826, 27riotaeqbidv 6273 . . . . . . . . 9
29 breq1 4398 . . . . . . . . . . . . . . 15
3029notbid 301 . . . . . . . . . . . . . 14
3130cbvralv 3005 . . . . . . . . . . . . 13
3231a1i 11 . . . . . . . . . . . 12
33 breq2 4399 . . . . . . . . . . . . . 14
3433notbid 301 . . . . . . . . . . . . 13
3534ralbidv 2829 . . . . . . . . . . . 12
3632, 35bitrd 261 . . . . . . . . . . 11
3736cbvriotav 6281 . . . . . . . . . 10
3837a1i 11 . . . . . . . . 9
3928, 38eqtrd 2505 . . . . . . . 8
4039cbvmptv 4488 . . . . . . 7
4124, 40eqtri 2493 . . . . . 6
4241rnmptss 6068 . . . . 5
4323, 42syl 17 . . . 4
4411, 43ssexd 4543 . . . . 5
45 elpwg 3950 . . . . 5
4644, 45syl 17 . . . 4
4743, 46mpbird 240 . . 3
48 dffn3 5748 . . . . . . . . . 10
4948biimpi 199 . . . . . . . . 9
503, 49syl 17 . . . . . . . 8
5150, 43fssresd 5762 . . . . . . 7
52 simpl 464 . . . . . . . . 9
53 simprl 772 . . . . . . . . 9
54 simprr 774 . . . . . . . . 9
55 simpl 464 . . . . . . . . . . 11
56 fvres 5893 . . . . . . . . . . . . . . 15
5756eqcomd 2477 . . . . . . . . . . . . . 14
5857ad2antrr 740 . . . . . . . . . . . . 13
59 simpr 468 . . . . . . . . . . . . 13
60 fvres 5893 . . . . . . . . . . . . . 14
6160ad2antlr 741 . . . . . . . . . . . . 13
6258, 59, 613eqtrd 2509 . . . . . . . . . . . 12
63623adantl1 1186 . . . . . . . . . . 11
64 simpl1 1033 . . . . . . . . . . . . . 14
65 simpl3 1035 . . . . . . . . . . . . . 14
66 vex 3034 . . . . . . . . . . . . . . . . . . 19
6741elrnmpt 5087 . . . . . . . . . . . . . . . . . . 19
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . 18
6968biimpi 199 . . . . . . . . . . . . . . . . 17
7069adantr 472 . . . . . . . . . . . . . . . 16
71703ad2antl2 1193 . . . . . . . . . . . . . . 15
7271, 68sylibr 217 . . . . . . . . . . . . . 14
73 id 22 . . . . . . . . . . . . . . . 16
7473eqcomd 2477 . . . . . . . . . . . . . . 15
7574adantl 473 . . . . . . . . . . . . . 14
76 eleq1 2537 . . . . . . . . . . . . . . . . . 18
77763anbi3d 1371 . . . . . . . . . . . . . . . . 17
78 fveq2 5879 . . . . . . . . . . . . . . . . . 18
7978eqeq2d 2481 . . . . . . . . . . . . . . . . 17
8077, 79anbi12d 725 . . . . . . . . . . . . . . . 16
81 breq1 4398 . . . . . . . . . . . . . . . . 17
8281notbid 301 . . . . . . . . . . . . . . . 16
8380, 82imbi12d 327 . . . . . . . . . . . . . . 15
84 eleq1 2537 . . . . . . . . . . . . . . . . . . 19
85843anbi2d 1370 . . . . . . . . . . . . . . . . . 18
86 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
8786eqeq1d 2473 . . . . . . . . . . . . . . . . . 18
8885, 87anbi12d 725 . . . . . . . . . . . . . . . . 17
89 breq2 4399 . . . . . . . . . . . . . . . . . 18
9089notbid 301 . . . . . . . . . . . . . . . . 17
9188, 90imbi12d 327 . . . . . . . . . . . . . . . 16
92 eleq1 2537 . . . . . . . . . . . . . . . . . . . 20
93923anbi3d 1371 . . . . . . . . . . . . . . . . . . 19
94 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
9594eqeq2d 2481 . . . . . . . . . . . . . . . . . . 19
9693, 95anbi12d 725 . . . . . . . . . . . . . . . . . 18
97 breq1 4398 . . . . . . . . . . . . . . . . . . 19
9897notbid 301 . . . . . . . . . . . . . . . . . 18
9996, 98imbi12d 327 . . . . . . . . . . . . . . . . 17
100 eleq1 2537 . . . . . . . . . . . . . . . . . . . . 21
1011003anbi2d 1370 . . . . . . . . . . . . . . . . . . . 20
102 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
103102eqeq1d 2473 . . . . . . . . . . . . . . . . . . . 20
104101, 103anbi12d 725 . . . . . . . . . . . . . . . . . . 19
105 breq2 4399 . . . . . . . . . . . . . . . . . . . 20
106105notbid 301 . . . . . . . . . . . . . . . . . . 19
107104, 106imbi12d 327 . . . . . . . . . . . . . . . . . 18
108 nfv 1769 . . . . . . . . . . . . . . . . . . . . . 22
109 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . 23
110 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . . . . . . 25
11141, 110nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . . . . 24
112111nfrn 5083 . . . . . . . . . . . . . . . . . . . . . . 23
113109, 112nfel 2624 . . . . . . . . . . . . . . . . . . . . . 22
114112nfcri 2606 . . . . . . . . . . . . . . . . . . . . . 22
115108, 113, 114nf3an 2033 . . . . . . . . . . . . . . . . . . . . 21
116 nfv 1769 . . . . . . . . . . . . . . . . . . . . 21
117115, 116nfan 2031 . . . . . . . . . . . . . . . . . . . 20
118 nfv 1769 . . . . . . . . . . . . . . . . . . . 20
119 simp3 1032 . . . . . . . . . . . . . . . . . . . . . . . . 25
120119eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . 24
121 simp11 1060 . . . . . . . . . . . . . . . . . . . . . . . . . 26
122 simp2 1031 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
124 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
125124notbid 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126125ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127126cbvriotav 6281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
128127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129123, 128eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1301293ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
131126cbvreuv 3007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
13219, 131sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133 riota1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1351343adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136130, 135mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
137136simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
138121, 122, 119, 137syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . 25
139121, 122, 19syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25
140126riota2 6292 . . . . . . . . . . . . . . . . . . . . . . . . 25
141138, 139, 140syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24
142120, 141mpbird 240 . . . . . . . . . . . . . . . . . . . . . . 23
1431423adant1r 1285 . . . . . . . . . . . . . . . . . . . . . 22
14443sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1451443adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . 26
146145adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
1471463ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . 24
14874ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1491483adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . 25
150 fniniseg 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
151121, 3, 1503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
152138, 151mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
153152simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1541533adant1r 1285 . . . . . . . . . . . . . . . . . . . . . . . . 25
155149, 154eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . 24
156147, 155jca 541 . . . . . . . . . . . . . . . . . . . . . . 23
157 fniniseg 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1583, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1591583ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . 25
160159ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24
1611603adant3 1050 . . . . . . . . . . . . . . . . . . . . . . 23
162156, 161mpbird 240 . . . . . . . . . . . . . . . . . . . . . 22
163 rspa 2774 . . . . . . . . . . . . . . . . . . . . . 22
164143, 162, 163syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21
1651643exp 1230 . . . . . . . . . . . . . . . . . . . 20
166117, 118, 165rexlimd 2866 . . . . . . . . . . . . . . . . . . 19
16771, 166mpd 15 . . . . . . . . . . . . . . . . . 18
168107, 167chvarv 2120 . . . . . . . . . . . . . . . . 17
16999, 168chvarv 2120 . . . . . . . . . . . . . . . 16
17091, 169chvarv 2120 . . . . . . . . . . . . . . 15
17183, 170chvarv 2120 . . . . . . . . . . . . . 14
17264, 65, 72, 75, 171syl31anc 1295 . . . . . . . . . . . . 13
173172, 167jca 541 . . . . . . . . . . . 12
174 weso 4830 . . . . . . . . . . . . . . . 16
1758, 174syl 17 . . . . . . . . . . . . . . 15
176175adantr 472 . . . . . . . . . . . . . 14
1771763ad2antl1 1192 . . . . . . . . . . . . 13
17843sselda 3418 . . . . . . . . . . . . . . 15
1791783adant3 1050 . . . . . . . . . . . . . 14
180179adantr 472 . . . . . . . . . . . . 13
181 sotrieq2 4788 . . . . . . . . . . . . 13
182177, 180, 146, 181syl12anc 1290 . . . . . . . . . . . 12
183173, 182mpbird 240 . . . . . . . . . . 11
18455, 63, 183syl2anc 673 . . . . . . . . . 10
185184ex 441 . . . . . . . . 9
18652, 53, 54, 185syl3anc 1292 . . . . . . . 8
187186ralrimivva 2814 . . . . . . 7
18851, 187jca 541 . . . . . 6
189 dff13 6177 . . . . . 6
190188, 189sylibr 217 . . . . 5
191 riotaex 6274 . . . . . . . . . . . . . 14
192191rgenw 2768 . . . . . . . . . . . . 13
193192a1i 11 . . . . . . . . . . . 12
19441fnmpt 5714 . . . . . . . . . . . 12
195193, 194syl 17 . . . . . . . . . . 11
196 dffn3 5748 . . . . . . . . . . . 12
197196biimpi 199 . . . . . . . . . . 11
198195, 197syl 17 . . . . . . . . . 10
199198ffvelrnda 6037 . . . . . . . . 9
200 fvres 5893 . . . . . . . . . . 11
201199, 200syl 17 . . . . . . . . . 10
20217, 15sylibr 217 . . . . . . . . . . . . . 14
203191a1i 11 . . . . . . . . . . . . . 14
20441fvmpt2 5972 . . . . . . . . . . . . . 14
205202, 203, 204syl2anc 673 . . . . . . . . . . . . 13
206205, 21eqeltrd 2549 . . . . . . . . . . . 12
207 fvex 5889 . . . . . . . . . . . . . 14
208 eleq1 2537 . . . . . . . . . . . . . . . 16
209 eleq1 2537 . . . . . . . . . . . . . . . . 17
210 fveq2 5879 . . . . . . . . . . . . . . . . . 18
211210eqeq1d 2473 . . . . . . . . . . . . . . . . 17
212209, 211anbi12d 725 . . . . . . . . . . . . . . . 16
213208, 212bibi12d 328 . . . . . . . . . . . . . . 15
214213imbi2d 323 . . . . . . . . . . . . . 14
2153, 150syl 17 . . . . . . . . . . . . . 14
216207, 214, 215vtocl 3086 . . . . . . . . . . . . 13
217216adantr 472 . . . . . . . . . . . 12
218206, 217mpbid 215 . . . . . . . . . . 11
219218simprd 470 . . . . . . . . . 10
220201, 219eqtr2d 2506 . . . . . . . . 9
221 fveq2 5879 . . . . . . . . . . 11
222221eqeq2d 2481 . . . . . . . . . 10
223222rspcev 3136 . . . . . . . . 9
224199, 220, 223syl2anc 673 . . . . . . . 8
225224ralrimiva 2809 . . . . . . 7
22651, 225jca 541 . . . . . 6
227 dffo3 6052 . . . . . 6
228226, 227sylibr 217 . . . . 5
229190, 228jca 541 . . . 4
230 df-f1o 5596 . . . 4
231229, 230sylibr 217 . . 3
232 nfcv 2612 . . . . . 6
233 nfcv 2612 . . . . . . . . 9
234 nfriota1 6277 . . . . . . . . 9
235233, 234nfmpt 4484 . . . . . . . 8
23641, 235nfcxfr 2610 . . . . . . 7
237236nfrn 5083 . . . . . 6
238232, 237nfres 5113 . . . . 5
239238, 237, 233nff1o 5826 . . . 4
240 reseq2 5106 . . . . 5
241 id 22 . . . . 5
242 eqidd 2472 . . . . 5
243240, 241, 242f1oeq123d 5824 . . . 4
244239, 243rspce 3131 . . 3
24547, 231, 244syl2anc 673 . 2
246 reseq2 5106 . . . 4
247 id 22 . . . 4
248 eqidd 2472 . . . 4
249246, 247, 248f1oeq123d 5824 . . 3
250249cbvrexv 3006 . 2
251245, 250sylib 201 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  wrex 2757  wreu 2758  cvv 3031   wss 3390  c0 3722  cpw 3942  csn 3959   class class class wbr 4395   cmpt 4454   wor 4759   wwe 4797  ccnv 4838   cdm 4839   crn 4840   cres 4841  cima 4842   wfn 5584  wf 5585  wf1 5586  wfo 5587  wf1o 5588  cfv 5589  crio 6269 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270 This theorem is referenced by:  wessf1orn  37531
 Copyright terms: Public domain W3C validator