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

Theorem cofsmo 7895
 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 by Mario Carneiro, 20-Mar-2013.)
Hypotheses
Ref Expression
cofsmo.1
cofsmo.2
cofsmo.3 OrdIso
Assertion
Ref Expression
cofsmo
Distinct variable groups:   ,,,,,,   ,,,,,,   ,   ,,,   ,,,,
Allowed substitution hints:   ()   ()   (,,,,,)   (,,,)   (,,)

Proof of Theorem cofsmo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cofsmo.1 . . . . . . . . . . . . 13
2 ssrab2 3258 . . . . . . . . . . . . 13
31, 2eqsstri 3208 . . . . . . . . . . . 12
4 ssexg 4160 . . . . . . . . . . . 12
53, 4mpan 651 . . . . . . . . . . 11
6 onss 4582 . . . . . . . . . . . . 13
73, 6syl5ss 3190 . . . . . . . . . . . 12
8 epweon 4575 . . . . . . . . . . . 12
9 wess 4380 . . . . . . . . . . . 12
107, 8, 9ee10 1366 . . . . . . . . . . 11
11 cofsmo.3 . . . . . . . . . . . 12 OrdIso
1211oiiso 7252 . . . . . . . . . . 11
135, 10, 12syl2anc 642 . . . . . . . . . 10
1413ad2antlr 707 . . . . . . . . 9
15 isof1o 5822 . . . . . . . . 9
16 f1ofo 5479 . . . . . . . . 9
1714, 15, 163syl 18 . . . . . . . 8
18 fof 5451 . . . . . . . . 9
19 fss 5397 . . . . . . . . 9
2018, 3, 19sylancl 643 . . . . . . . 8
2117, 20syl 15 . . . . . . 7
2211oion 7251 . . . . . . . . . 10
235, 22syl 15 . . . . . . . . 9
2423ad2antlr 707 . . . . . . . 8
25 simplr 731 . . . . . . . 8
26 eloni 4402 . . . . . . . . . . 11
27 smoiso2 6386 . . . . . . . . . . 11
2826, 7, 27syl2an 463 . . . . . . . . . 10
2928biimpar 471 . . . . . . . . 9
3029simprd 449 . . . . . . . 8
3124, 25, 14, 30syl21anc 1181 . . . . . . 7
32 eloni 4402 . . . . . . . 8
3332ad2antlr 707 . . . . . . 7
34 smorndom 6385 . . . . . . 7
3521, 31, 33, 34syl3anc 1182 . . . . . 6
36 onsssuc 4480 . . . . . . 7
3724, 25, 36syl2anc 642 . . . . . 6
3835, 37mpbid 201 . . . . 5
3938adantrr 697 . . . 4
40 vex 2791 . . . . . 6
4111oiexg 7250 . . . . . . . 8
425, 41syl 15 . . . . . . 7
4342ad2antlr 707 . . . . . 6
44 coexg 5215 . . . . . 6
4540, 43, 44sylancr 644 . . . . 5
46 simprl 732 . . . . . . 7
4721adantrr 697 . . . . . . 7
48 fco 5398 . . . . . . 7
4946, 47, 48syl2anc 642 . . . . . 6
50 simpr 447 . . . . . . . . 9
5150, 21, 48syl2anc 642 . . . . . . . 8
52 ordsson 4581 . . . . . . . . 9
5352ad2antrr 706 . . . . . . . 8
5424, 26syl 15 . . . . . . . 8
5517, 18syl 15 . . . . . . . . . . . 12
56 simpl 443 . . . . . . . . . . . 12
57 ffvelrn 5663 . . . . . . . . . . . 12
5855, 56, 57syl2an 463 . . . . . . . . . . 11
59 ffn 5389 . . . . . . . . . . . . . 14
6017, 18, 593syl 18 . . . . . . . . . . . . 13
6160, 31jca 518 . . . . . . . . . . . 12
62 smoel2 6380 . . . . . . . . . . . 12
6361, 62sylan 457 . . . . . . . . . . 11
64 fveq2 5525 . . . . . . . . . . . . . . . 16
6564eleq2d 2350 . . . . . . . . . . . . . . 15
6665raleqbi1dv 2744 . . . . . . . . . . . . . 14
67 fveq2 5525 . . . . . . . . . . . . . . . . . . 19
6867eleq1d 2349 . . . . . . . . . . . . . . . . . 18
6968cbvralv 2764 . . . . . . . . . . . . . . . . 17
70 fveq2 5525 . . . . . . . . . . . . . . . . . . 19
7170eleq2d 2350 . . . . . . . . . . . . . . . . . 18
7271raleqbi1dv 2744 . . . . . . . . . . . . . . . . 17
7369, 72syl5bb 248 . . . . . . . . . . . . . . . 16
7473cbvrabv 2787 . . . . . . . . . . . . . . 15
751, 74eqtri 2303 . . . . . . . . . . . . . 14
7666, 75elrab2 2925 . . . . . . . . . . . . 13
7776simprbi 450 . . . . . . . . . . . 12
78 fveq2 5525 . . . . . . . . . . . . . 14
7978eleq1d 2349 . . . . . . . . . . . . 13
8079rspccv 2881 . . . . . . . . . . . 12
8177, 80syl 15 . . . . . . . . . . 11
8258, 63, 81sylc 56 . . . . . . . . . 10
8321adantr 451 . . . . . . . . . . . 12
84 ordtr1 4435 . . . . . . . . . . . . . . 15
8584ancomsd 440 . . . . . . . . . . . . . 14
8624, 26, 853syl 18 . . . . . . . . . . . . 13
8786imp 418 . . . . . . . . . . . 12
88 fvco3 5596 . . . . . . . . . . . 12
8983, 87, 88syl2anc 642 . . . . . . . . . . 11
90 simprl 732 . . . . . . . . . . . 12
91 fvco3 5596 . . . . . . . . . . . 12
9283, 90, 91syl2anc 642 . . . . . . . . . . 11
9389, 92eleq12d 2351 . . . . . . . . . 10
9482, 93mpbird 223 . . . . . . . . 9
9594ralrimivva 2635 . . . . . . . 8
96 issmo2 6366 . . . . . . . . 9
9796imp 418 . . . . . . . 8
9851, 53, 54, 95, 97syl13anc 1184 . . . . . . 7
9998adantrr 697 . . . . . 6
10017adantr 451 . . . . . . . . . . 11
101 rabn0 3474 . . . . . . . . . . . . . . . . . 18
102 ssrab2 3258 . . . . . . . . . . . . . . . . . . . 20
103102, 6syl5ss 3190 . . . . . . . . . . . . . . . . . . 19
104 cofsmo.2 . . . . . . . . . . . . . . . . . . . . 21
105 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . 24
106105sseq2d 3206 . . . . . . . . . . . . . . . . . . . . . . 23
107106cbvrabv 2787 . . . . . . . . . . . . . . . . . . . . . 22
108107inteqi 3866 . . . . . . . . . . . . . . . . . . . . 21
109104, 108eqtri 2303 . . . . . . . . . . . . . . . . . . . 20
110 onint 4586 . . . . . . . . . . . . . . . . . . . 20
111109, 110syl5eqel 2367 . . . . . . . . . . . . . . . . . . 19
112103, 111sylan 457 . . . . . . . . . . . . . . . . . 18
113101, 112sylan2br 462 . . . . . . . . . . . . . . . . 17
114 fveq2 5525 . . . . . . . . . . . . . . . . . . 19
115114sseq2d 3206 . . . . . . . . . . . . . . . . . 18
116115elrab 2923 . . . . . . . . . . . . . . . . 17
117113, 116sylib 188 . . . . . . . . . . . . . . . 16
118117ex 423 . . . . . . . . . . . . . . 15
119118adantl 452 . . . . . . . . . . . . . 14
120 simpr2 962 . . . . . . . . . . . . . . . . . 18
121 simp3 957 . . . . . . . . . . . . . . . . . . . . 21
122109eleq2i 2347 . . . . . . . . . . . . . . . . . . . . . 22
123 simp21 988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
124 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125124, 52syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
126 fss 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
127123, 125, 126syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26
128 simp22 989 . . . . . . . . . . . . . . . . . . . . . . . . . 26
129 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130127, 128, 129syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25
131 simp1r 980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
132 ontr1 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1331323impib 1149 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
134131, 121, 128, 133syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26
135 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . 26
136127, 134, 135syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25
137 ontri1 4426 . . . . . . . . . . . . . . . . . . . . . . . . 25
138130, 136, 137syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24
139 simp23 990 . . . . . . . . . . . . . . . . . . . . . . . . 25
140 simpl1 958 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
141140, 103syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
142 sstr 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
143133, 142anim12i 549 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
144 rabid 2716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
145143, 144sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
146 onnmin 4594 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
147141, 145, 146syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26
148147expr 598 . . . . . . . . . . . . . . . . . . . . . . . . 25
149131, 121, 128, 139, 148syl31anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24
150138, 149sylbird 226 . . . . . . . . . . . . . . . . . . . . . . 23
151150con4d 97 . . . . . . . . . . . . . . . . . . . . . 22
152122, 151syl5bi 208 . . . . . . . . . . . . . . . . . . . . 21
153121, 152mpd 14 . . . . . . . . . . . . . . . . . . . 20
1541533expia 1153 . . . . . . . . . . . . . . . . . . 19
155154ralrimiv 2625 . . . . . . . . . . . . . . . . . 18
156 fveq2 5525 . . . . . . . . . . . . . . . . . . . . 21
157156eleq2d 2350 . . . . . . . . . . . . . . . . . . . 20
158157raleqbi1dv 2744 . . . . . . . . . . . . . . . . . . 19
159158, 1elrab2 2925 . . . . . . . . . . . . . . . . . 18
160120, 155, 159sylanbrc 645 . . . . . . . . . . . . . . . . 17
161160expcom 424 . . . . . . . . . . . . . . . 16
1621613expib 1154 . . . . . . . . . . . . . . 15
163162com13 74 . . . . . . . . . . . . . 14
164119, 163syld 40 . . . . . . . . . . . . 13
165164com23 72 . . . . . . . . . . . 12
166165imp31 421 . . . . . . . . . . 11
167 foelrn 5679 . . . . . . . . . . 11
168100, 166, 167syl2anc 642 . . . . . . . . . 10
169 simpllr 735 . . . . . . . . . . . . . 14
170 eleq1 2343 . . . . . . . . . . . . . . . . 17
171170biimpcd 215 . . . . . . . . . . . . . . . 16
172 fveq2 5525 . . . . . . . . . . . . . . . . . . 19
173172sseq2d 3206 . . . . . . . . . . . . . . . . . 18
17467sseq2d 3206 . . . . . . . . . . . . . . . . . . 19
175174cbvrabv 2787 . . . . . . . . . . . . . . . . . 18
176173, 175elrab2 2925 . . . . . . . . . . . . . . . . 17
177176simprbi 450 . . . . . . . . . . . . . . . 16
178171, 177syl6 29 . . . . . . . . . . . . . . 15
179113, 178syl 15 . . . . . . . . . . . . . 14
180169, 179sylancom 648 . . . . . . . . . . . . 13
181180adantr 451 . . . . . . . . . . . 12
18221ad2antrr 706 . . . . . . . . . . . . . 14
183 fvco3 5596 . . . . . . . . . . . . . 14
184182, 183sylancom 648 . . . . . . . . . . . . 13
185184sseq2d 3206 . . . . . . . . . . . 12
186181, 185sylibrd 225 . . . . . . . . . . 11
187186reximdva 2655 . . . . . . . . . 10
188168, 187mpd 14 . . . . . . . . 9
189188ex 423 . . . . . . . 8
190189ralimdv 2622 . . . . . . 7
191190impr 602 . . . . . 6
19249, 99, 1913jca 1132 . . . . 5
193 feq1 5375 . . . . . . 7
194 smoeq 6367 . . . . . . 7
195 fveq1 5524 . . . . . . . . . 10
196195sseq2d 3206 . . . . . . . . 9
197196rexbidv 2564 . . . . . . . 8
198197ralbidv 2563 . . . . . . 7
199193, 194, 1983anbi123d 1252 . . . . . 6
200199spcegv 2869 . . . . 5
20145, 192, 200sylc 56 . . . 4
202 feq2 5376 . . . . . . 7
203 rexeq 2737 . . . . . . . 8
204203ralbidv 2563 . . . . . . 7
205202, 2043anbi13d 1254 . . . . . 6
206205exbidv 1612 . . . . 5
207206rspcev 2884 . . . 4
20839, 201, 207syl2anc 642 . . 3
209208ex 423 . 2
210209exlimdv 1664 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 934  wex 1528   wceq 1623   wcel 1684   wne 2446  wral 2543  wrex 2544  crab 2547  cvv 2788   wss 3152  c0 3455  cint 3862   cep 4303   wwe 4351   word 4391  con0 4392   csuc 4394   cdm 4689   ccom 4693   wfn 5250  wf 5251  wfo 5253  wf1o 5254  cfv 5255   wiso 5256   wsmo 6362  OrdIsocoi 7224 This theorem is referenced by:  cfcof  7900 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-riota 6304  df-smo 6363  df-recs 6388  df-oi 7225
 Copyright terms: Public domain W3C validator