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

Theorem wemapweOLD 8161
 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 8160 as of 3-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
wemapweOLD.t
wemapweOLD.u
wemapweOLD.2
wemapweOLD.3
wemapweOLD.4
wemapweOLD.5
wemapweOLD.6
wemapweOLD.7
Assertion
Ref Expression
wemapweOLD
Distinct variable groups:   ,,,,   ,,   ,,,,   ,,   ,,   ,,   ,S   ,,   ,

Proof of Theorem wemapweOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wemapweOLD.u . . . . . . . . 9
2 eqid 2457 . . . . . . . . 9
3 eqid 2457 . . . . . . . . 9
4 simprr 757 . . . . . . . . . . 11
5 wemapweOLD.2 . . . . . . . . . . . 12
65adantr 465 . . . . . . . . . . 11
7 wemapweOLD.5 . . . . . . . . . . . 12
87oiiso 7983 . . . . . . . . . . 11
94, 6, 8syl2anc 661 . . . . . . . . . 10
10 isof1o 6221 . . . . . . . . . 10
119, 10syl 16 . . . . . . . . 9
12 simprl 756 . . . . . . . . . . 11
13 wemapweOLD.3 . . . . . . . . . . . 12
1413adantr 465 . . . . . . . . . . 11
15 wemapweOLD.6 . . . . . . . . . . . 12
1615oiiso 7983 . . . . . . . . . . 11
1712, 14, 16syl2anc 661 . . . . . . . . . 10
18 isof1o 6221 . . . . . . . . . 10
19 f1ocnv 5833 . . . . . . . . . 10
2017, 18, 193syl 20 . . . . . . . . 9
217oiexg 7981 . . . . . . . . . . 11
2221ad2antll 728 . . . . . . . . . 10
23 dmexg 6731 . . . . . . . . . 10
2422, 23syl 16 . . . . . . . . 9
2515oiexg 7981 . . . . . . . . . . 11
2625ad2antrl 727 . . . . . . . . . 10
27 dmexg 6731 . . . . . . . . . 10
2826, 27syl 16 . . . . . . . . 9
29 wemapweOLD.7 . . . . . . . . . 10
3017, 18syl 16 . . . . . . . . . . . . . . 15
31 f1ofo 5828 . . . . . . . . . . . . . . 15
32 forn 5803 . . . . . . . . . . . . . . 15
3330, 31, 323syl 20 . . . . . . . . . . . . . 14
34 wemapweOLD.4 . . . . . . . . . . . . . . 15
3534adantr 465 . . . . . . . . . . . . . 14
3633, 35eqnetrd 2750 . . . . . . . . . . . . 13
37 dm0rn0 5224 . . . . . . . . . . . . . 14
3837necon3bii 2725 . . . . . . . . . . . . 13
3936, 38sylibr 212 . . . . . . . . . . . 12
4015oicl 7975 . . . . . . . . . . . . 13
41 ord0eln0 4937 . . . . . . . . . . . . 13
4240, 41ax-mp 5 . . . . . . . . . . . 12
4339, 42sylibr 212 . . . . . . . . . . 11
4415oif 7976 . . . . . . . . . . . 12
4544ffvelrni 6030 . . . . . . . . . . 11
4643, 45syl 16 . . . . . . . . . 10
4729, 46syl5eqel 2549 . . . . . . . . 9
481, 2, 3, 11, 20, 4, 12, 24, 28, 47mapfienOLD 8159 . . . . . . . 8
49 eqid 2457 . . . . . . . . . . 11
5015oion 7982 . . . . . . . . . . . 12
5150ad2antrl 727 . . . . . . . . . . 11
527oion 7982 . . . . . . . . . . . 12
5352ad2antll 728 . . . . . . . . . . 11
5449, 51, 53cantnfdmOLD 8104 . . . . . . . . . 10
5529fveq2i 5874 . . . . . . . . . . . . . . . . 17
56 f1ocnvfv1 6182 . . . . . . . . . . . . . . . . . 18
5730, 43, 56syl2anc 661 . . . . . . . . . . . . . . . . 17
5855, 57syl5eq 2510 . . . . . . . . . . . . . . . 16
5958sneqd 4041 . . . . . . . . . . . . . . 15
60 df1o2 7161 . . . . . . . . . . . . . . 15
6159, 60syl6eqr 2516 . . . . . . . . . . . . . 14
6261difeq2d 3621 . . . . . . . . . . . . 13
6362imaeq2d 5342 . . . . . . . . . . . 12
6463eleq1d 2526 . . . . . . . . . . 11
6564rabbidv 3101 . . . . . . . . . 10
6654, 65eqtr4d 2501 . . . . . . . . 9
67 f1oeq3 5814 . . . . . . . . 9
6866, 67syl 16 . . . . . . . 8
6948, 68mpbird 232 . . . . . . 7
70 eqid 2457 . . . . . . . . 9
71 eqid 2457 . . . . . . . . 9
7270, 51, 53, 71oemapwe 8134 . . . . . . . 8
7372simpld 459 . . . . . . 7
74 eqid 2457 . . . . . . . 8
7574f1owe 6249 . . . . . . 7
7669, 73, 75sylc 60 . . . . . 6
77 weinxp 5072 . . . . . 6
7876, 77sylib 196 . . . . 5
7911adantr 465 . . . . . . . . . . . 12
80 f1ofn 5822 . . . . . . . . . . . 12
81 fveq2 5871 . . . . . . . . . . . . . . 15
82 fveq2 5871 . . . . . . . . . . . . . . 15
8381, 82breq12d 4465 . . . . . . . . . . . . . 14
84 breq1 4455 . . . . . . . . . . . . . . . 16
8584imbi1d 317 . . . . . . . . . . . . . . 15
8685ralbidv 2896 . . . . . . . . . . . . . 14
8783, 86anbi12d 710 . . . . . . . . . . . . 13
8887rexrn 6033 . . . . . . . . . . . 12
8979, 80, 883syl 20 . . . . . . . . . . 11
90 f1ofo 5828 . . . . . . . . . . . . 13
91 forn 5803 . . . . . . . . . . . . 13
9279, 90, 913syl 20 . . . . . . . . . . . 12
9392rexeqdv 3061 . . . . . . . . . . 11
9426adantr 465 . . . . . . . . . . . . . . 15
95 cnvexg 6746 . . . . . . . . . . . . . . 15
9694, 95syl 16 . . . . . . . . . . . . . 14
97 vex 3112 . . . . . . . . . . . . . . 15
9822adantr 465 . . . . . . . . . . . . . . 15
99 coexg 6751 . . . . . . . . . . . . . . 15
10097, 98, 99sylancr 663 . . . . . . . . . . . . . 14
101 coexg 6751 . . . . . . . . . . . . . 14
10296, 100, 101syl2anc 661 . . . . . . . . . . . . 13
103 vex 3112 . . . . . . . . . . . . . . 15
104 coexg 6751 . . . . . . . . . . . . . . 15
105103, 98, 104sylancr 663 . . . . . . . . . . . . . 14
106 coexg 6751 . . . . . . . . . . . . . 14
10796, 105, 106syl2anc 661 . . . . . . . . . . . . 13
108 fveq1 5870 . . . . . . . . . . . . . . . . 17
109 fveq1 5870 . . . . . . . . . . . . . . . . 17
110 eleq12 2533 . . . . . . . . . . . . . . . . 17
111108, 109, 110syl2an 477 . . . . . . . . . . . . . . . 16
112 fveq1 5870 . . . . . . . . . . . . . . . . . . 19
113 fveq1 5870 . . . . . . . . . . . . . . . . . . 19
114112, 113eqeqan12d 2480 . . . . . . . . . . . . . . . . . 18
115114imbi2d 316 . . . . . . . . . . . . . . . . 17
116115ralbidv 2896 . . . . . . . . . . . . . . . 16
117111, 116anbi12d 710 . . . . . . . . . . . . . . 15
118117rexbidv 2968 . . . . . . . . . . . . . 14
119118, 71brabga 4766 . . . . . . . . . . . . 13
120102, 107, 119syl2anc 661 . . . . . . . . . . . 12
121 simprl 756 . . . . . . . . . . . . . 14
122 coeq1 5165 . . . . . . . . . . . . . . . 16
123122coeq2d 5170 . . . . . . . . . . . . . . 15
124 eqid 2457 . . . . . . . . . . . . . . 15
125123, 124fvmptg 5954 . . . . . . . . . . . . . 14
126121, 102, 125syl2anc 661 . . . . . . . . . . . . 13
127 simprr 757 . . . . . . . . . . . . . 14
128 coeq1 5165 . . . . . . . . . . . . . . . 16
129128coeq2d 5170 . . . . . . . . . . . . . . 15
130129, 124fvmptg 5954 . . . . . . . . . . . . . 14
131127, 107, 130syl2anc 661 . . . . . . . . . . . . 13
132126, 131breq12d 4465 . . . . . . . . . . . 12
13317ad2antrr 725 . . . . . . . . . . . . . . . . . 18
134 isocnv 6226 . . . . . . . . . . . . . . . . . 18
135133, 134syl 16 . . . . . . . . . . . . . . . . 17
136 ssrab2 3584 . . . . . . . . . . . . . . . . . . . . 21
1371, 136eqsstri 3533 . . . . . . . . . . . . . . . . . . . 20
138137, 121sseldi 3501 . . . . . . . . . . . . . . . . . . 19
139 elmapi 7460 . . . . . . . . . . . . . . . . . . 19
140138, 139syl 16 . . . . . . . . . . . . . . . . . 18
1417oif 7976 . . . . . . . . . . . . . . . . . . 19
142141ffvelrni 6030 . . . . . . . . . . . . . . . . . 18
143 ffvelrn 6029 . . . . . . . . . . . . . . . . . 18
144140, 142, 143syl2an 477 . . . . . . . . . . . . . . . . 17
145137, 127sseldi 3501 . . . . . . . . . . . . . . . . . . 19
146 elmapi 7460 . . . . . . . . . . . . . . . . . . 19
147145, 146syl 16 . . . . . . . . . . . . . . . . . 18
148 ffvelrn 6029 . . . . . . . . . . . . . . . . . 18
149147, 142, 148syl2an 477 . . . . . . . . . . . . . . . . 17
150 isorel 6222 . . . . . . . . . . . . . . . . 17
151135, 144, 149, 150syl12anc 1226 . . . . . . . . . . . . . . . 16
152 fvex 5881 . . . . . . . . . . . . . . . . 17
153152epelc 4798 . . . . . . . . . . . . . . . 16
154151, 153syl6bb 261 . . . . . . . . . . . . . . 15
155140adantr 465 . . . . . . . . . . . . . . . . . . 19
156 fco 5746 . . . . . . . . . . . . . . . . . . 19
157155, 141, 156sylancl 662 . . . . . . . . . . . . . . . . . 18
158 fvco3 5950 . . . . . . . . . . . . . . . . . 18