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

Theorem wemapwe 8160
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.) (Revised by AV, 3-Jul-2019.)
Hypotheses
Ref Expression
wemapwe.t
wemapwe.u
wemapwe.2
wemapwe.3
wemapwe.4
wemapwe.5
wemapwe.6
wemapwe.7
Assertion
Ref Expression
wemapwe
Distinct variable groups:   , , , ,   , ,   , , , ,   , ,   , ,   , ,   ,S   , ,   ,

Proof of Theorem wemapwe
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wemapwe.u . . . . . . . . 9
2 eqid 2457 . . . . . . . . 9
3 eqid 2457 . . . . . . . . 9
4 simprr 757 . . . . . . . . . . 11
5 wemapwe.2 . . . . . . . . . . . 12
65adantr 465 . . . . . . . . . . 11
7 wemapwe.5 . . . . . . . . . . . 12
87oiiso 7983 . . . . . . . . . . 11
94, 6, 8syl2anc 661 . . . . . . . . . 10
10 isof1o 6221 . . . . . . . . . 10
119, 10syl 16 . . . . . . . . 9
12 simprl 756 . . . . . . . . . . 11
13 wemapwe.3 . . . . . . . . . . . 12
1413adantr 465 . . . . . . . . . . 11
15 wemapwe.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 wemapwe.7 . . . . . . . . . 10
3017, 18syl 16 . . . . . . . . . . . . . . 15
31 f1ofo 5828 . . . . . . . . . . . . . . 15
32 forn 5803 . . . . . . . . . . . . . . 15
3330, 31, 323syl 20 . . . . . . . . . . . . . 14
34 wemapwe.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, 47mapfien 7887 . . . . . . . 8
49 eqid 2457 . . . . . . . . . . 11
5015oion 7982 . . . . . . . . . . . 12
5150ad2antrl 727 . . . . . . . . . . 11
527oion 7982 . . . . . . . . . . . 12
5352ad2antll 728 . . . . . . . . . . 11
5449, 51, 53cantnfdm 8102 . . . . . . . . . 10
5529fveq2i 5874 . . . . . . . . . . . . 13
56 f1ocnvfv1 6182 . . . . . . . . . . . . . 14
5730, 43, 56syl2anc 661 . . . . . . . . . . . . 13
5855, 57syl5eq 2510 . . . . . . . . . . . 12
5958breq2d 4464 . . . . . . . . . . 11
6059rabbidv 3101 . . . . . . . . . 10
6154, 60eqtr4d 2501 . . . . . . . . 9
62 f1oeq3 5814 . . . . . . . . 9
6361, 62syl 16 . . . . . . . 8
6448, 63mpbird 232 . . . . . . 7
65 eqid 2457 . . . . . . . . 9
66 eqid 2457 . . . . . . . . 9
6765, 51, 53, 66oemapwe 8134 . . . . . . . 8
6867simpld 459 . . . . . . 7
69 eqid 2457 . . . . . . . 8
7069f1owe 6249 . . . . . . 7
7164, 68, 70sylc 60 . . . . . 6
72 weinxp 5072 . . . . . 6
7371, 72sylib 196 . . . . 5
7411adantr 465 . . . . . . . . . . . 12
75 f1ofn 5822 . . . . . . . . . . . 12
76 fveq2 5871 . . . . . . . . . . . . . . 15
77 fveq2 5871 . . . . . . . . . . . . . . 15
7876, 77breq12d 4465 . . . . . . . . . . . . . 14
79 breq1 4455 . . . . . . . . . . . . . . . 16
8079imbi1d 317 . . . . . . . . . . . . . . 15
8180ralbidv 2896 . . . . . . . . . . . . . 14
8278, 81anbi12d 710 . . . . . . . . . . . . 13
8382rexrn 6033 . . . . . . . . . . . 12
8474, 75, 833syl 20 . . . . . . . . . . 11
85 f1ofo 5828 . . . . . . . . . . . . 13
86 forn 5803 . . . . . . . . . . . . 13
8774, 85, 863syl 20 . . . . . . . . . . . 12
8887rexeqdv 3061 . . . . . . . . . . 11
8926adantr 465 . . . . . . . . . . . . . . 15
90 cnvexg 6746 . . . . . . . . . . . . . . 15
9189, 90syl 16 . . . . . . . . . . . . . 14
92 vex 3112 . . . . . . . . . . . . . . 15
9322adantr 465 . . . . . . . . . . . . . . 15
94 coexg 6751 . . . . . . . . . . . . . . 15
9592, 93, 94sylancr 663 . . . . . . . . . . . . . 14
96 coexg 6751 . . . . . . . . . . . . . 14
9791, 95, 96syl2anc 661 . . . . . . . . . . . . 13
98 vex 3112 . . . . . . . . . . . . . . 15
99 coexg 6751 . . . . . . . . . . . . . . 15
10098, 93, 99sylancr 663 . . . . . . . . . . . . . 14
101 coexg 6751 . . . . . . . . . . . . . 14
10291, 100, 101syl2anc 661 . . . . . . . . . . . . 13
103 fveq1 5870 . . . . . . . . . . . . . . . . 17
104 fveq1 5870 . . . . . . . . . . . . . . . . 17
105 eleq12 2533 . . . . . . . . . . . . . . . . 17
106103, 104, 105syl2an 477 . . . . . . . . . . . . . . . 16
107 fveq1 5870 . . . . . . . . . . . . . . . . . . 19
108 fveq1 5870 . . . . . . . . . . . . . . . . . . 19
109107, 108eqeqan12d 2480 . . . . . . . . . . . . . . . . . 18
110109imbi2d 316 . . . . . . . . . . . . . . . . 17
111110ralbidv 2896 . . . . . . . . . . . . . . . 16
112106, 111anbi12d 710 . . . . . . . . . . . . . . 15
113112rexbidv 2968 . . . . . . . . . . . . . 14
114113, 66brabga 4766 . . . . . . . . . . . . 13
11597, 102, 114syl2anc 661 . . . . . . . . . . . 12
116 simprl 756 . . . . . . . . . . . . . 14
117 coeq1 5165 . . . . . . . . . . . . . . . 16
118117coeq2d 5170 . . . . . . . . . . . . . . 15
119 eqid 2457 . . . . . . . . . . . . . . 15
120118, 119fvmptg 5954 . . . . . . . . . . . . . 14
121116, 97, 120syl2anc 661 . . . . . . . . . . . . 13
122 simprr 757 . . . . . . . . . . . . . 14
123 coeq1 5165 . . . . . . . . . . . . . . . 16
124123coeq2d 5170 . . . . . . . . . . . . . . 15
125124, 119fvmptg 5954 . . . . . . . . . . . . . 14
126122, 102, 125syl2anc 661 . . . . . . . . . . . . 13
127121, 126breq12d 4465 . . . . . . . . . . . 12
12817ad2antrr 725 . . . . . . . . . . . . . . . . . 18
129 isocnv 6226 . . . . . . . . . . . . . . . . . 18
130128, 129syl 16 . . . . . . . . . . . . . . . . 17
131 ssrab2 3584 . . . . . . . . . . . . . . . . . . . . 21
1321, 131eqsstri 3533 . . . . . . . . . . . . . . . . . . . 20
133132, 116sseldi 3501 . . . . . . . . . . . . . . . . . . 19
134 elmapi 7460 . . . . . . . . . . . . . . . . . . 19
135133, 134syl 16 . . . . . . . . . . . . . . . . . 18
1367oif 7976 . . . . . . . . . . . . . . . . . . 19
137136ffvelrni 6030 . . . . . . . . . . . . . . . . . 18
138 ffvelrn 6029 . . . . . . . . . . . . . . . . . 18
139135, 137, 138syl2an 477 . . . . . . . . . . . . . . . . 17
140132, 122sseldi 3501 . . . . . . . . . . . . . . . . . . 19
141 elmapi 7460 . . . . . . . . . . . . . . . . . . 19
142140, 141syl 16 . . . . . . . . . . . . . . . . . 18
143 ffvelrn 6029 . . . . . . . . . . . . . . . . . 18
144142, 137, 143syl2an 477 . . . . . . . . . . . . . . . . 17
145 isorel 6222 . . . . . . . . . . . . . . . . 17
146130, 139, 144, 145syl12anc 1226 . . . . . . . . . . . . . . . 16
147 fvex 5881 . . . . . . . . . . . . . . . . 17
148147epelc 4798 . . . . . . . . . . . . . . . 16
149146, 148syl6bb 261 . . . . . . . . . . . . . . 15
150135adantr 465 . . . . . . . . . . . . . . . . . . 19
151 fco 5746 . . . . . . . . . . . . . . . . . . 19
152150, 136, 151sylancl 662 . . . . . . . . . . . . . . . . . 18
153 fvco3 5950 . . . . . . . . . . . . . . . . . 18
154152, 153sylancom 667 . . . . . . . . . . . . . . . . 17
155 simpr 461 . . . . . . . . . . . . . . . . . . 19
156 fvco3 5950 . . . . . . . . . . . . . . . . . . 19
157136, 155, 156sylancr 663 . . . . . . . . . . . . . . . . . 18
158157fveq2d 5875 . . . . . . . . . . . . . . . . 17