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

Theorem rankcf 8652
 Description: Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of form a cofinal map into . (Contributed by Mario Carneiro, 27-May-2013.)
Assertion
Ref Expression
rankcf

Proof of Theorem rankcf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rankon 7721 . . 3
2 onzsl 4826 . . 3
31, 2mpbi 200 . 2
4 sdom0 7239 . . . 4
5 fveq2 5728 . . . . . 6
6 cf0 8131 . . . . . 6
75, 6syl6eq 2484 . . . . 5
87breq2d 4224 . . . 4
94, 8mtbiri 295 . . 3
10 fveq2 5728 . . . . . . 7
11 cfsuc 8137 . . . . . . 7
1210, 11sylan9eqr 2490 . . . . . 6
13 nsuceq0 4661 . . . . . . . . 9
14 neeq1 2609 . . . . . . . . 9
1513, 14mpbiri 225 . . . . . . . 8
16 fveq2 5728 . . . . . . . . . . 11
17 0elon 4634 . . . . . . . . . . . . 13
18 r1fnon 7693 . . . . . . . . . . . . . 14
19 fndm 5544 . . . . . . . . . . . . . 14
2018, 19ax-mp 8 . . . . . . . . . . . . 13
2117, 20eleqtrri 2509 . . . . . . . . . . . 12
22 rankonid 7755 . . . . . . . . . . . 12
2321, 22mpbi 200 . . . . . . . . . . 11
2416, 23syl6eq 2484 . . . . . . . . . 10
2524necon3i 2643 . . . . . . . . 9
26 rankvaln 7725 . . . . . . . . . . 11
2726necon1ai 2646 . . . . . . . . . 10
28 breq2 4216 . . . . . . . . . . 11
29 neeq1 2609 . . . . . . . . . . 11
30 0sdom1dom 7306 . . . . . . . . . . . 12
31 vex 2959 . . . . . . . . . . . . 13
32310sdom 7238 . . . . . . . . . . . 12
3330, 32bitr3i 243 . . . . . . . . . . 11
3428, 29, 33vtoclbg 3012 . . . . . . . . . 10
3527, 34syl 16 . . . . . . . . 9
3625, 35mpbird 224 . . . . . . . 8
3715, 36syl 16 . . . . . . 7
3837adantl 453 . . . . . 6
3912, 38eqbrtrd 4232 . . . . 5
4039rexlimiva 2825 . . . 4
41 domnsym 7233 . . . 4
4240, 41syl 16 . . 3
43 nlim0 4639 . . . . . . . . . . . . . . . . 17
44 limeq 4593 . . . . . . . . . . . . . . . . 17
4543, 44mtbiri 295 . . . . . . . . . . . . . . . 16
4626, 45syl 16 . . . . . . . . . . . . . . 15
4746con4i 124 . . . . . . . . . . . . . 14
48 r1elssi 7731 . . . . . . . . . . . . . 14
4947, 48syl 16 . . . . . . . . . . . . 13
5049sselda 3348 . . . . . . . . . . . 12
51 ranksnb 7753 . . . . . . . . . . . 12
5250, 51syl 16 . . . . . . . . . . 11
53 rankelb 7750 . . . . . . . . . . . . . 14
5447, 53syl 16 . . . . . . . . . . . . 13
55 limsuc 4829 . . . . . . . . . . . . 13
5654, 55sylibd 206 . . . . . . . . . . . 12
5756imp 419 . . . . . . . . . . 11
5852, 57eqeltrd 2510 . . . . . . . . . 10
59 eleq1a 2505 . . . . . . . . . 10
6058, 59syl 16 . . . . . . . . 9
6160rexlimdva 2830 . . . . . . . 8
6261abssdv 3417 . . . . . . 7
63 snex 4405 . . . . . . . . . . . . 13
6463dfiun2 4125 . . . . . . . . . . . 12
65 iunid 4146 . . . . . . . . . . . 12
6664, 65eqtr3i 2458 . . . . . . . . . . 11
6766fveq2i 5731 . . . . . . . . . 10
6848sselda 3348 . . . . . . . . . . . . . . 15
69 snwf 7735 . . . . . . . . . . . . . . 15
70 eleq1a 2505 . . . . . . . . . . . . . . 15
7168, 69, 703syl 19 . . . . . . . . . . . . . 14
7271rexlimdva 2830 . . . . . . . . . . . . 13
7372abssdv 3417 . . . . . . . . . . . 12
74 abrexexg 5984 . . . . . . . . . . . . 13
75 eleq1 2496 . . . . . . . . . . . . . 14
76 sseq1 3369 . . . . . . . . . . . . . 14
77 vex 2959 . . . . . . . . . . . . . . 15
7877r1elss 7732 . . . . . . . . . . . . . 14
7975, 76, 78vtoclbg 3012 . . . . . . . . . . . . 13
8074, 79syl 16 . . . . . . . . . . . 12
8173, 80mpbird 224 . . . . . . . . . . 11
82 rankuni2b 7779 . . . . . . . . . . 11
8381, 82syl 16 . . . . . . . . . 10
8467, 83syl5eqr 2482 . . . . . . . . 9
85 fvex 5742 . . . . . . . . . . 11
8685dfiun2 4125 . . . . . . . . . 10
87 fveq2 5728 . . . . . . . . . . . 12
8863, 87abrexco 5986 . . . . . . . . . . 11
8988unieqi 4025 . . . . . . . . . 10
9086, 89eqtri 2456 . . . . . . . . 9
9184, 90syl6req 2485 . . . . . . . 8
9247, 91syl 16 . . . . . . 7
93 fvex 5742 . . . . . . . 8
9493cfslb 8146 . . . . . . 7
9562, 92, 94mpd3an23 1281 . . . . . 6
96 fveq2 5728 . . . . . . . . . . 11
9796fveq2d 5732 . . . . . . . . . 10
98 breq12 4217 . . . . . . . . . 10
9997, 98mpdan 650 . . . . . . . . 9
100 rexeq 2905 . . . . . . . . . . 11
101100abbidv 2550 . . . . . . . . . 10
102 breq12 4217 . . . . . . . . . 10
103101, 102mpancom 651 . . . . . . . . 9
10499, 103imbi12d 312 . . . . . . . 8
105 eqid 2436 . . . . . . . . . 10
106105rnmpt 5116 . . . . . . . . 9
107 cfon 8135 . . . . . . . . . . 11
108 sdomdom 7135 . . . . . . . . . . 11
109 ondomen 7918 . . . . . . . . . . 11
110107, 108, 109sylancr 645 . . . . . . . . . 10
111 fvex 5742 . . . . . . . . . . . 12
112111, 105fnmpti 5573 . . . . . . . . . . 11
113 dffn4 5659 . . . . . . . . . . 11
114112, 113mpbi 200 . . . . . . . . . 10
115 fodomnum 7938 . . . . . . . . . 10
116110, 114, 115ee10 1385 . . . . . . . . 9
117106, 116syl5eqbrr 4246 . . . . . . . 8
118104, 117vtoclg 3011 . . . . . . 7
11947, 118syl 16 . . . . . 6
120 domtr 7160 . . . . . . 7
121120, 41syl 16 . . . . . 6
12295, 119, 121ee12an 1372 . . . . 5
123122pm2.01d 163 . . . 4