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

Theorem cofsmo 8670
Description: Any cofinal map implies the existence of a strictly monotone cofinal map with a domain no larger than the original. Proposition 11.7 of [TakeutiZaring] p. 101. (Contributed by Mario Carneiro, 20-Mar-2013.)
Hypotheses
Ref Expression
cofsmo.1
cofsmo.2
cofsmo.3
Assertion
Ref Expression
cofsmo
Distinct variable groups:   , , , , , ,   , , , , , ,   ,   , , ,   ,O, , ,

Proof of Theorem cofsmo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cofsmo.1 . . . . . . . . . . . . 13
2 ssrab2 3584 . . . . . . . . . . . . 13
31, 2eqsstri 3533 . . . . . . . . . . . 12
4 ssexg 4598 . . . . . . . . . . . 12
53, 4mpan 670 . . . . . . . . . . 11
6 onss 6626 . . . . . . . . . . . . 13
73, 6syl5ss 3514 . . . . . . . . . . . 12
8 epweon 6619 . . . . . . . . . . . 12
9 wess 4871 . . . . . . . . . . . 12
107, 8, 9mpisyl 18 . . . . . . . . . . 11
11 cofsmo.3 . . . . . . . . . . . 12
1211oiiso 7983 . . . . . . . . . . 11
135, 10, 12syl2anc 661 . . . . . . . . . 10
1413ad2antlr 726 . . . . . . . . 9
15 isof1o 6221 . . . . . . . . 9
16 f1ofo 5828 . . . . . . . . 9
1714, 15, 163syl 20 . . . . . . . 8
18 fof 5800 . . . . . . . . 9
19 fss 5744 . . . . . . . . 9
2018, 3, 19sylancl 662 . . . . . . . 8
2117, 20syl 16 . . . . . . 7
2211oion 7982 . . . . . . . . . 10
235, 22syl 16 . . . . . . . . 9
2423ad2antlr 726 . . . . . . . 8
25 simplr 755 . . . . . . . 8
26 eloni 4893 . . . . . . . . . . 11
27 smoiso2 7059 . . . . . . . . . . 11
2826, 7, 27syl2an 477 . . . . . . . . . 10
2928biimpar 485 . . . . . . . . 9
3029simprd 463 . . . . . . . 8
3124, 25, 14, 30syl21anc 1227 . . . . . . 7
32 eloni 4893 . . . . . . . 8
3332ad2antlr 726 . . . . . . 7
34 smorndom 7058 . . . . . . 7
3521, 31, 33, 34syl3anc 1228 . . . . . 6
36 onsssuc 4970 . . . . . . 7
3724, 25, 36syl2anc 661 . . . . . 6
3835, 37mpbid 210 . . . . 5
3938adantrr 716 . . . 4
40 vex 3112 . . . . . 6
4111oiexg 7981 . . . . . . . 8
425, 41syl 16 . . . . . . 7
4342ad2antlr 726 . . . . . 6
44 coexg 6751 . . . . . 6
4540, 43, 44sylancr 663 . . . . 5
46 simprl 756 . . . . . . 7
4721adantrr 716 . . . . . . 7
48 fco 5746 . . . . . . 7
4946, 47, 48syl2anc 661 . . . . . 6
50 simpr 461 . . . . . . . . 9
5150, 21, 48syl2anc 661 . . . . . . . 8
52 ordsson 6625 . . . . . . . . 9
5352ad2antrr 725 . . . . . . . 8
5424, 26syl 16 . . . . . . . 8
5517, 18syl 16 . . . . . . . . . . . 12
56 simpl 457 . . . . . . . . . . . 12
57 ffvelrn 6029 . . . . . . . . . . . 12
5855, 56, 57syl2an 477 . . . . . . . . . . 11
59 ffn 5736 . . . . . . . . . . . . . 14
6017, 18, 593syl 20 . . . . . . . . . . . . 13
6160, 31jca 532 . . . . . . . . . . . 12
62 smoel2 7053 . . . . . . . . . . . 12
6361, 62sylan 471 . . . . . . . . . . 11
64 fveq2 5871 . . . . . . . . . . . . . . . 16
6564eleq2d 2527 . . . . . . . . . . . . . . 15
6665raleqbi1dv 3062 . . . . . . . . . . . . . 14
67 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
6867eleq1d 2526 . . . . . . . . . . . . . . . . . 18
6968cbvralv 3084 . . . . . . . . . . . . . . . . 17
70 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
7170eleq2d 2527 . . . . . . . . . . . . . . . . . 18
7271raleqbi1dv 3062 . . . . . . . . . . . . . . . . 17
7369, 72syl5bb 257 . . . . . . . . . . . . . . . 16
7473cbvrabv 3108 . . . . . . . . . . . . . . 15
751, 74eqtri 2486 . . . . . . . . . . . . . 14
7666, 75elrab2 3259 . . . . . . . . . . . . 13
7776simprbi 464 . . . . . . . . . . . 12
78 fveq2 5871 . . . . . . . . . . . . . 14
7978eleq1d 2526 . . . . . . . . . . . . 13
8079rspccv 3207 . . . . . . . . . . . 12
8177, 80syl 16 . . . . . . . . . . 11
8258, 63, 81sylc 60 . . . . . . . . . 10
8321adantr 465 . . . . . . . . . . 11
84 ordtr1 4926 . . . . . . . . . . . . . 14
8584ancomsd 454 . . . . . . . . . . . . 13
8624, 26, 853syl 20 . . . . . . . . . . . 12
8786imp 429 . . . . . . . . . . 11
88 fvco3 5950 . . . . . . . . . . 11
8983, 87, 88syl2anc 661 . . . . . . . . . 10
90 simprl 756 . . . . . . . . . . 11
91 fvco3 5950 . . . . . . . . . . 11
9283, 90, 91syl2anc 661 . . . . . . . . . 10
9382, 89, 923eltr4d 2560 . . . . . . . . 9
9493ralrimivva 2878 . . . . . . . 8
95 issmo2 7039 . . . . . . . . 9
9695imp 429 . . . . . . . 8
9751, 53, 54, 94, 96syl13anc 1230 . . . . . . 7
9897adantrr 716 . . . . . 6
9917adantr 465 . . . . . . . . . . 11
100 rabn0 3805 . . . . . . . . . . . . . . . . . 18
101 ssrab2 3584 . . . . . . . . . . . . . . . . . . . 20
102101, 6syl5ss 3514 . . . . . . . . . . . . . . . . . . 19
103 cofsmo.2 . . . . . . . . . . . . . . . . . . . . 21
104 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . 24
105104sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . 23
106105cbvrabv 3108 . . . . . . . . . . . . . . . . . . . . . 22
107106inteqi 4290 . . . . . . . . . . . . . . . . . . . . 21
108103, 107eqtri 2486 . . . . . . . . . . . . . . . . . . . 20
109 onint 6630 . . . . . . . . . . . . . . . . . . . 20
110108, 109syl5eqel 2549 . . . . . . . . . . . . . . . . . . 19
111102, 110sylan 471 . . . . . . . . . . . . . . . . . 18
112100, 111sylan2br 476 . . . . . . . . . . . . . . . . 17
113 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
114113sseq2d 3531 . . . . . . . . . . . . . . . . . 18
115114elrab 3257 . . . . . . . . . . . . . . . . 17
116112, 115sylib 196 . . . . . . . . . . . . . . . 16
117116ex 434 . . . . . . . . . . . . . . 15
118117adantl 466 . . . . . . . . . . . . . 14
119 simpr2 1003 . . . . . . . . . . . . . . . . . 18
120 simp3 998 . . . . . . . . . . . . . . . . . . . . 21
121108eleq2i 2535 . . . . . . . . . . . . . . . . . . . . . 22
122 simp21 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
123 simp1l 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
124123, 52syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
125122, 124fssd 5745 . . . . . . . . . . . . . . . . . . . . . . . . . 26
126 simp22 1030 . . . . . . . . . . . . . . . . . . . . . . . . . 26
127125, 126ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . . . . . . 25
128 simp1r 1021 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
129 ontr1 4929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1301293impib 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
131128, 120, 126, 130syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . 26
132125, 131ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . . . . . . 25
133 ontri1 4917 . . . . . . . . . . . . . . . . . . . . . . . . 25
134127, 132, 133syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
135 simp23 1031 . . . . . . . . . . . . . . . . . . . . . . . . 25
136 simpl1 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137136, 102syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
138 sstr 3511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
139130, 138anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140 rabid 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
141139, 140sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
142 onnmin 6638 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
143137, 141, 142syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
144143expr 615 . . . . . . . . . . . . . . . . . . . . . . . . 25
145128, 120, 126, 135, 144syl31anc 1231 . . . . . . . . . . . . . . . . . . . . . . . 24
146134, 145sylbird 235 . . . . . . . . . . . . . . . . . . . . . . 23
147146con4d 105 . . . . . . . . . . . . . . . . . . . . . 22
148121, 147syl5bi 217 . . . . . . . . . . . . . . . . . . . . 21
149120, 148mpd 15 . . . . . . . . . . . . . . . . . . . 20
1501493expia 1198 . . . . . . . . . . . . . . . . . . 19
151150ralrimiv 2869 . . . . . . . . . . . . . . . . . 18
152 fveq2 5871 . . . . . . . . . . . . . . . . . . . . 21
153152eleq2d 2527 . . . . . . . . . . . . . . . . . . . 20
154153raleqbi1dv 3062 . . . . . . . . . . . . . . . . . . 19
155154, 1elrab2 3259 . . . . . . . . . . . . . . . . . 18
156119, 151, 155sylanbrc 664 . . . . . . . . . . . . . . . . 17
157156expcom 435 . . . . . . . . . . . . . . . 16
1581573expib 1199 . . . . . . . . . . . . . . 15
159158com13 80 . . . . . . . . . . . . . 14
160118, 159syld 44 . . . . . . . . . . . . 13
161160com23 78 . . . . . . . . . . . 12
162161imp31 432 . . . . . . . . . . 11
163 foelrn 6050 . . . . . . . . . . 11
16499, 162, 163syl2anc 661 . . . . . . . . . 10
165 simpllr 760 . . . . . . . . . . . . . 14
166 eleq1 2529 . . . . . . . . . . . . . . . . 17
167166biimpcd 224 . . . . . . . . . . . . . . . 16
168 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
169168sseq2d 3531 . . . . . . . . . . . . . . . . . 18
17067sseq2d 3531 . . . . . . . . . . . . . . . . . . 19
171170cbvrabv 3108 . . . . . . . . . . . . . . . . . 18
172169, 171elrab2 3259 . . . . . . . . . . . . . . . . 17
173172simprbi 464 . . . . . . . . . . . . . . . 16
174167, 173syl6 33 . . . . . . . . . . . . . . 15
175112, 174syl 16 . . . . . . . . . . . . . 14
176165, 175sylancom 667 . . . . . . . . . . . . 13
177176adantr 465 . . . . . . . . . . . 12
17821ad2antrr 725 . . . . . . . . . . . . . 14
179 fvco3 5950 . . . . . . . . . . . . . 14
180178, 179sylancom 667 . . . . . . . . . . . . 13
181180sseq2d 3531 . . . . . . . . . . . 12
182177, 181sylibrd 234 . . . . . . . . . . 11
183182reximdva 2932 . . . . . . . . . 10
184164, 183mpd 15 . . . . . . . . 9
185184ex 434 . . . . . . . 8
186185ralimdv 2867 . . . . . . 7
187186impr 619 . . . . . 6
18849, 98, 1873jca 1176 . . . . 5
189 feq1 5718 . . . . . . 7
190 smoeq 7040 . . . . . . 7
191 fveq1 5870 . . . . . . . . . 10
192191sseq2d 3531 . . . . . . . . 9
193192rexbidv 2968 . . . . . . . 8
194193ralbidv 2896 . . . . . . 7
195189, 190, 1943anbi123d 1299 . . . . . 6
196195spcegv 3195 . . . . 5