Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  wemapweOLD Structured version   Unicode version

Theorem wemapweOLD 8141
 Description: Construct lexicographic order on a function space based on a reverse well-ordering of the indexes and a well-ordering of the values. (Contributed by Mario Carneiro, 29-May-2015.) Obsolete version of wemapwe 8140 as of 3-Jul-2019. (New usage is discouraged.)
Hypotheses
Ref Expression
wemapweOLD.t
wemapweOLD.u
wemapweOLD.2
wemapweOLD.3
wemapweOLD.4
wemapweOLD.5 OrdIso
wemapweOLD.6 OrdIso
wemapweOLD.7
Assertion
Ref Expression
wemapweOLD
Distinct variable groups:   ,,,,   ,,   ,,,,   ,,   ,,   ,,   ,   ,,   ,
Allowed substitution hints:   (,)   (,)   (,)   (,,)   (,,,)   (,)   (,)   (,,)

Proof of Theorem wemapweOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wemapweOLD.u . . . . . . . . 9
2 eqid 2467 . . . . . . . . 9
3 eqid 2467 . . . . . . . . 9
4 simprr 756 . . . . . . . . . . 11
5 wemapweOLD.2 . . . . . . . . . . . 12
65adantr 465 . . . . . . . . . . 11
7 wemapweOLD.5 . . . . . . . . . . . 12 OrdIso
87oiiso 7963 . . . . . . . . . . 11
94, 6, 8syl2anc 661 . . . . . . . . . 10
10 isof1o 6210 . . . . . . . . . 10
119, 10syl 16 . . . . . . . . 9
12 simprl 755 . . . . . . . . . . 11
13 wemapweOLD.3 . . . . . . . . . . . 12
1413adantr 465 . . . . . . . . . . 11
15 wemapweOLD.6 . . . . . . . . . . . 12 OrdIso
1615oiiso 7963 . . . . . . . . . . 11
1712, 14, 16syl2anc 661 . . . . . . . . . 10
18 isof1o 6210 . . . . . . . . . 10
19 f1ocnv 5828 . . . . . . . . . 10
2017, 18, 193syl 20 . . . . . . . . 9
217oiexg 7961 . . . . . . . . . . 11
2221ad2antll 728 . . . . . . . . . 10
23 dmexg 6716 . . . . . . . . . 10
2422, 23syl 16 . . . . . . . . 9
2515oiexg 7961 . . . . . . . . . . 11
2625ad2antrl 727 . . . . . . . . . 10
27 dmexg 6716 . . . . . . . . . 10
2826, 27syl 16 . . . . . . . . 9
29 wemapweOLD.7 . . . . . . . . . 10
3017, 18syl 16 . . . . . . . . . . . . . . 15
31 f1ofo 5823 . . . . . . . . . . . . . . 15
32 forn 5798 . . . . . . . . . . . . . . 15
3330, 31, 323syl 20 . . . . . . . . . . . . . 14
34 wemapweOLD.4 . . . . . . . . . . . . . . 15
3534adantr 465 . . . . . . . . . . . . . 14
3633, 35eqnetrd 2760 . . . . . . . . . . . . 13
37 dm0rn0 5219 . . . . . . . . . . . . . 14
3837necon3bii 2735 . . . . . . . . . . . . 13
3936, 38sylibr 212 . . . . . . . . . . . 12
4015oicl 7955 . . . . . . . . . . . . 13
41 ord0eln0 4932 . . . . . . . . . . . . 13
4240, 41ax-mp 5 . . . . . . . . . . . 12
4339, 42sylibr 212 . . . . . . . . . . 11
4415oif 7956 . . . . . . . . . . . 12
4544ffvelrni 6021 . . . . . . . . . . 11
4643, 45syl 16 . . . . . . . . . 10
4729, 46syl5eqel 2559 . . . . . . . . 9
481, 2, 3, 11, 20, 4, 12, 24, 28, 47mapfienOLD 8139 . . . . . . . 8
49 eqid 2467 . . . . . . . . . . 11
5015oion 7962 . . . . . . . . . . . 12
5150ad2antrl 727 . . . . . . . . . . 11
527oion 7962 . . . . . . . . . . . 12
5352ad2antll 728 . . . . . . . . . . 11
5449, 51, 53cantnfdmOLD 8084 . . . . . . . . . 10 CNF
5529fveq2i 5869 . . . . . . . . . . . . . . . . 17
56 f1ocnvfv1 6171 . . . . . . . . . . . . . . . . . 18
5730, 43, 56syl2anc 661 . . . . . . . . . . . . . . . . 17
5855, 57syl5eq 2520 . . . . . . . . . . . . . . . 16
5958sneqd 4039 . . . . . . . . . . . . . . 15
60 df1o2 7143 . . . . . . . . . . . . . . 15
6159, 60syl6eqr 2526 . . . . . . . . . . . . . 14
6261difeq2d 3622 . . . . . . . . . . . . 13
6362imaeq2d 5337 . . . . . . . . . . . 12
6463eleq1d 2536 . . . . . . . . . . 11
6564rabbidv 3105 . . . . . . . . . 10
6654, 65eqtr4d 2511 . . . . . . . . 9 CNF
67 f1oeq3 5809 . . . . . . . . 9 CNF CNF
6866, 67syl 16 . . . . . . . 8 CNF
6948, 68mpbird 232 . . . . . . 7 CNF
70 eqid 2467 . . . . . . . . 9 CNF CNF
71 eqid 2467 . . . . . . . . 9
7270, 51, 53, 71oemapwe 8114 . . . . . . . 8 CNF OrdIso CNF
7372simpld 459 . . . . . . 7 CNF
74 eqid 2467 . . . . . . . 8
7574f1owe 6238 . . . . . . 7 CNF CNF
7669, 73, 75sylc 60 . . . . . 6
77 weinxp 5067 . . . . . 6
7876, 77sylib 196 . . . . 5
7911adantr 465 . . . . . . . . . . . 12
80 f1ofn 5817 . . . . . . . . . . . 12
81 fveq2 5866 . . . . . . . . . . . . . . 15
82 fveq2 5866 . . . . . . . . . . . . . . 15
8381, 82breq12d 4460 . . . . . . . . . . . . . 14
84 breq1 4450 . . . . . . . . . . . . . . . 16
8584imbi1d 317 . . . . . . . . . . . . . . 15
8685ralbidv 2903 . . . . . . . . . . . . . 14
8783, 86anbi12d 710 . . . . . . . . . . . . 13
8887rexrn 6024 . . . . . . . . . . . 12
8979, 80, 883syl 20 . . . . . . . . . . 11
90 f1ofo 5823 . . . . . . . . . . . . 13
91 forn 5798 . . . . . . . . . . . . 13
9279, 90, 913syl 20 . . . . . . . . . . . 12
9392rexeqdv 3065 . . . . . . . . . . 11
9426adantr 465 . . . . . . . . . . . . . . 15
95 cnvexg 6731 . . . . . . . . . . . . . . 15
9694, 95syl 16 . . . . . . . . . . . . . 14
97 vex 3116 . . . . . . . . . . . . . . 15
9822adantr 465 . . . . . . . . . . . . . . 15
99 coexg 6736 . . . . . . . . . . . . . . 15
10097, 98, 99sylancr 663 . . . . . . . . . . . . . 14
101 coexg 6736 . . . . . . . . . . . . . 14
10296, 100, 101syl2anc 661 . . . . . . . . . . . . 13
103 vex 3116 . . . . . . . . . . . . . . 15
104 coexg 6736 . . . . . . . . . . . . . . 15
105103, 98, 104sylancr 663 . . . . . . . . . . . . . 14
106 coexg 6736 . . . . . . . . . . . . . 14
10796, 105, 106syl2anc 661 . . . . . . . . . . . . 13
108 fveq1 5865 . . . . . . . . . . . . . . . . 17
109 fveq1 5865 . . . . . . . . . . . . . . . . 17
110 eleq12 2543 . . . . . . . . . . . . . . . . 17
111108, 109, 110syl2an 477 . . . . . . . . . . . . . . . 16
112 fveq1 5865 . . . . . . . . . . . . . . . . . . 19
113 fveq1 5865 . . . . . . . . . . . . . . . . . . 19
114112, 113eqeqan12d 2490 . . . . . . . . . . . . . . . . . 18
115114imbi2d 316 . . . . . . . . . . . . . . . . 17
116115ralbidv 2903 . . . . . . . . . . . . . . . 16
117111, 116anbi12d 710 . . . . . . . . . . . . . . 15
118117rexbidv 2973 . . . . . . . . . . . . . 14
119118, 71brabga 4761 . . . . . . . . . . . . 13
120102, 107, 119syl2anc 661 . . . . . . . . . . . 12
121 simprl 755 . . . . . . . . . . . . . 14
122 coeq1 5160 . . . . . . . . . . . . . . . 16
123122coeq2d 5165 . . . . . . . . . . . . . . 15
124 eqid 2467 . . . . . . . . . . . . . . 15
125123, 124fvmptg 5949 . . . . . . . . . . . . . 14
126121, 102, 125syl2anc 661 . . . . . . . . . . . . 13
127 simprr 756 . . . . . . . . . . . . . 14
128 coeq1 5160 . . . . . . . . . . . . . . . 16
129128coeq2d 5165 . . . . . . . . . . . . . . 15
130129, 124fvmptg 5949 . . . . . . . . . . . . . 14
131127, 107, 130syl2anc 661 . . . . . . . . . . . . 13
132126, 131breq12d 4460 . . . . . . . . . . . 12
13317ad2antrr 725 . . . . . . . . . . . . . . . . . 18
134 isocnv 6215 . . . . . . . . . . . . . . . . . 18
135133, 134syl 16 . . . . . . . . . . . . . . . . 17
136 ssrab2 3585 . . . . . . . . . . . . . . . . . . . . 21
1371, 136eqsstri 3534 . . . . . . . . . . . . . . . . . . . 20
138137, 121sseldi 3502 . . . . . . . . . . . . . . . . . . 19
139 elmapi 7441 . . . . . . . . . . . . . . . . . . 19
140138, 139syl 16 . . . . . . . . . . . . . . . . . 18
1417oif 7956 . . . . . . . . . . . . . . . . . . 19
142141ffvelrni 6021 . . . . . . . . . . . . . . . . . 18
143 ffvelrn 6020 . . . . . . . . . . . . . . . . . 18
144140, 142, 143syl2an 477 . . . . . . . . . . . . . . . . 17
145137, 127sseldi 3502 . . . . . . . . . . . . . . . . . . 19
146 elmapi 7441 . . . . . . . . . . . . . . . . . . 19
147145, 146syl 16 . . . . . . . . . . . . . . . . . 18
148 ffvelrn 6020 . . . . . . . . . . . . . . . . . 18
149147, 142, 148syl2an 477 . . . . . . . . . . . . . . . . 17
150 isorel 6211 . . . . . . . . . . . . . . . . 17
151135, 144, 149, 150syl12anc 1226 . . . . . . . . . . . . . . . 16
152 fvex 5876 . . . . . . . . . . . . . . . . 17
153152epelc 4793 . . . . . . . . . . . . . . . 16
154151, 153syl6bb 261 . . . . . . . . . . . . . . 15
155140adantr 465 . . . . . . . . . . . . . . . . . . 19
156 fco 5741 . . . . . . . . . . . . . . . . . . 19
157155, 141, 156sylancl 662 . . . . . . . . . . . . . . . . . 18
158 fvco3 5945 . . . . . . . . . . . . . . . . . 18
159157, 158sylancom 667 . . . . . . . . . . . . . . . . 17
160 simpr 461 . . . . . . . . . . . . . . . . . . 19
161 fvco3 5945 . . . . . . . . . . . . . . . . . . 19
162141, 160, 161sylancr 663 . . . . . . . . . . . . . . . . . 18
163162fveq2d 5870 . . . . . . . . . . . . . . . . 17
164159, 163eqtrd 2508 . . . . . . . . . . . . . . . 16
165147adantr 465 . . . . . . . . . . . . . . . . . . 19
166 fco 5741 . . . . . . . . . . . . . . . . . . 19
167165, 141, 166sylancl 662 . . . . . . . . . . . . . . . . . 18
168 fvco3 5945 . . . . . . . . . . . . . . . . . 18
169167, 168sylancom 667 . . . . . . . . . . . . . . . . 17
170 fvco3 5945 . . . . . . . . . . . . . . . . . . 19
171141, 160, 170sylancr 663 . . . . . . . . . . . . . . . . . 18
172171fveq2d 5870 . . . . . . . . . . . . . . . . 17
173169, 172eqtrd 2508 . . . . . . . . . . . . . . . 16
174164, 173eleq12d 2549 . . . . . . . . . . . . . . 15
175154, 174bitr4d 256 . . . . . . . . . . . . . 14
17692raleqdv 3064 . . . . . . . . . . . . . . . . 17
177 breq2 4451 . . . . . . . . . . . . . . . . . . . 20
178 fveq2 5866 . . . . . . . . . . . . . . . . . . . . 21
179 fveq2 5866 . . . . . . . . . . . . . . . . . . . . 21
180178, 179eqeq12d 2489 . . . . . . . . . . . . . . . . . . . 20
181177, 180imbi12d 320 . . . . . . . . . . . . . . . . . . 19
182181ralrn 6025 . . . . . . . . . . . . . . . . . 18
18379, 80, 1823syl 20 . . . . . . . . . . . . . . . . 17
184176, 183bitr3d 255 . . . . . . . . . . . . . . . 16
185184adantr 465 . . . . . . . . . . . . . . 15
186 epel 4794 . . . . . . . . . . . . . . . . . . 19
1879ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
188 isorel 6211 . . . . . . . . . . . . . . . . . . . 20
189187, 188sylancom 667 . . . . . . . . . . . . . . . . . . 19
190186, 189syl5bbr 259 . . . . . . . . . . . . . . . . . 18
191157adantrr 716 . . . . . . . . . . . . . . . . . . . . 21
192 simprr 756 . . . . . . . . . . . . . . . . . . . . 21
193 fvco3 5945 . . . . . . . . . . . . . . . . . . . . 21
194191, 192, 193syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
195167adantrr 716 . . . . . . . . . . . . . . . . . . . . 21
196 fvco3 5945 . . . . . . . . . . . . . . . . . . . . 21
197195, 192, 196syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
198194, 197eqeq12d 2489 . . . . . . . . . . . . . . . . . . 19
19930ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
200 f1of1 5815 . . . . . . . . . . . . . . . . . . . . 21
201199, 19, 2003syl 20 . . . . . . . . . . . . . . . . . . . 20
202191, 192ffvelrnd 6023 . . . . . . . . . . . . . . . . . . . 20
203195, 192ffvelrnd 6023 . . . . . . . . . . . . . . . . . . . 20
204 f1fveq 6159 . . . . . . . . . . . . . . . . . . . 20
205201, 202, 203, 204syl12anc 1226 . . . . . . . . . . . . . . . . . . 19
206 fvco3 5945 . . . . . . . . . . . . . . . . . . . . 21
207141, 192, 206sylancr 663 . . . . . . . . . . . . . . . . . . . 20
208 fvco3 5945 . . . . . . . . . . . . . . . . . . . . 21
209141, 192, 208sylancr 663 . . . . . . . . . . . . . . . . . . . 20
210207, 209eqeq12d 2489 . . . . . . . . . . . . . . . . . . 19
211198, 205, 2103bitrd 279 . . . . . . . . . . . . . . . . . 18
212190, 211imbi12d 320 . . . . . . . . . . . . . . . . 17
213212anassrs 648 . . . . . . . . . . . . . . . 16
214213ralbidva 2900 . . . . . . . . . . . . . . 15
215185, 214bitr4d 256 . . . . . . . . . . . . . 14
216175, 215anbi12d 710 . . . . . . . . . . . . 13
217216rexbidva 2970 . . . . . . . . . . . 12
218120, 132, 2173bitr4rd 286 . . . . . . . . . . 11
21989, 93, 2183bitr3d 283 . . . . . . . . . 10
220219ex 434 . . . . . . . . 9
221220pm5.32rd 640 . . . . . . . 8
222221opabbidv 4510 . . . . . . 7
223 wemapweOLD.t . . . . . . . . 9
224 df-xp 5005 . . . . . . . . 9
225223, 224ineq12i 3698 . . . . . . . 8
226 inopab 5133 . . . . . . . 8
227225, 226eqtri 2496 . . . . . . 7
228224ineq2i 3697 . . . . . . . 8
229 inopab 5133 . . . . . . . 8
230228, 229eqtri 2496 . . . . . . 7
231222, 227, 2303eqtr4g 2533 . . . . . 6
232 weeq1 4867 . . . . . 6
233231, 232syl 16 . . . . 5
23478, 233mpbird 232 . . . 4
235 weinxp 5067 . . . 4
236234, 235sylibr 212 . . 3
237236ex 434 . 2
238 we0 4874 . . 3
239 elmapex 7440 . . . . . . . . 9
240239con3i 135 . . . . . . . 8
241240pm2.21d 106 . . . . . . 7
242241ralrimiv 2876 . . . . . 6
243 rabeq0 3807 . . . . . 6
244242, 243sylibr 212 . . . . 5
2451, 244syl5eq 2520 . . . 4
246 weeq2 4868 . . . 4
247245, 246syl 16 . . 3
248238, 247mpbiri 233 . 2
249237, 248pm2.61d1 159 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   wceq 1379   wcel 1767   wne 2662  wral 2814  wrex 2815  crab 2818  cvv 3113   cdif 3473   cin 3475  c0 3785  csn 4027   class class class wbr 4447  copab 4504   cmpt 4505   cep 4789   wwe 4837   word 4877  con0 4878   cxp 4997  ccnv 4998   cdm 4999   crn 5000  cima 5002   ccom 5003   wfn 5583  wf 5584  wf1 5585  wfo 5586  wf1o 5587  cfv 5588   wiso 5589  (class class class)co 6285  c1o 7124   coe 7130   cmap 7421  cfn 7517  OrdIsocoi 7935   CNF ccnf 8079 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6246  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6903  df-recs 7043  df-rdg 7077  df-seqom 7114  df-1o 7131  df-2o 7132  df-oadd 7135  df-omul 7136  df-oexp 7137  df-er 7312  df-map 7423  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7831  df-oi 7936  df-cnf 8080 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator