Metamath Proof Explorer

Theorem rankcf

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

Ref Expression
Assertion rankcf ⊢¬A≺cf⁡rank⁡A

Proof

Step Hyp Ref Expression
1 rankon ⊢rank⁡A∈On
2 onzsl ⊢rank⁡A∈On↔rank⁡A=∅∨∃x∈Onrank⁡A=suc⁡x∨rank⁡A∈V∧Lim⁡rank⁡A
3 1 2 mpbi ⊢rank⁡A=∅∨∃x∈Onrank⁡A=suc⁡x∨rank⁡A∈V∧Lim⁡rank⁡A
4 sdom0 ⊢¬A≺∅
5 fveq2 ⊢rank⁡A=∅→cf⁡rank⁡A=cf⁡∅
6 cf0 ⊢cf⁡∅=∅
7 5 6 eqtrdi ⊢rank⁡A=∅→cf⁡rank⁡A=∅
8 7 breq2d ⊢rank⁡A=∅→A≺cf⁡rank⁡A↔A≺∅
9 4 8 mtbiri ⊢rank⁡A=∅→¬A≺cf⁡rank⁡A
10 fveq2 ⊢rank⁡A=suc⁡x→cf⁡rank⁡A=cf⁡suc⁡x
11 cfsuc ⊢x∈On→cf⁡suc⁡x=1𝑜
12 10 11 sylan9eqr ⊢x∈On∧rank⁡A=suc⁡x→cf⁡rank⁡A=1𝑜
13 nsuceq0 ⊢suc⁡x≠∅
14 neeq1 ⊢rank⁡A=suc⁡x→rank⁡A≠∅↔suc⁡x≠∅
15 13 14 mpbiri ⊢rank⁡A=suc⁡x→rank⁡A≠∅
16 fveq2 ⊢A=∅→rank⁡A=rank⁡∅
17 0elon ⊢∅∈On
18 r1fnon ⊢R1FnOn
19 18 fndmi ⊢dom⁡R1=On
20 17 19 eleqtrri ⊢∅∈dom⁡R1
21 rankonid ⊢∅∈dom⁡R1↔rank⁡∅=∅
22 20 21 mpbi ⊢rank⁡∅=∅
23 16 22 eqtrdi ⊢A=∅→rank⁡A=∅
24 23 necon3i ⊢rank⁡A≠∅→A≠∅
25 rankvaln ⊢¬A∈⋃R1On→rank⁡A=∅
26 25 necon1ai ⊢rank⁡A≠∅→A∈⋃R1On
27 breq2 ⊢y=A→1𝑜≼y↔1𝑜≼A
28 neeq1 ⊢y=A→y≠∅↔A≠∅
29 0sdom1dom ⊢∅≺y↔1𝑜≼y
30 vex ⊢y∈V
31 30 0sdom ⊢∅≺y↔y≠∅
32 29 31 bitr3i ⊢1𝑜≼y↔y≠∅
33 27 28 32 vtoclbg ⊢A∈⋃R1On→1𝑜≼A↔A≠∅
34 26 33 syl ⊢rank⁡A≠∅→1𝑜≼A↔A≠∅
35 24 34 mpbird ⊢rank⁡A≠∅→1𝑜≼A
36 15 35 syl ⊢rank⁡A=suc⁡x→1𝑜≼A
37 36 adantl ⊢x∈On∧rank⁡A=suc⁡x→1𝑜≼A
38 12 37 eqbrtrd ⊢x∈On∧rank⁡A=suc⁡x→cf⁡rank⁡A≼A
39 38 rexlimiva ⊢∃x∈Onrank⁡A=suc⁡x→cf⁡rank⁡A≼A
40 domnsym ⊢cf⁡rank⁡A≼A→¬A≺cf⁡rank⁡A
41 39 40 syl ⊢∃x∈Onrank⁡A=suc⁡x→¬A≺cf⁡rank⁡A
42 nlim0 ⊢¬Lim⁡∅
43 limeq ⊢rank⁡A=∅→Lim⁡rank⁡A↔Lim⁡∅
44 42 43 mtbiri ⊢rank⁡A=∅→¬Lim⁡rank⁡A
45 25 44 syl ⊢¬A∈⋃R1On→¬Lim⁡rank⁡A
46 45 con4i ⊢Lim⁡rank⁡A→A∈⋃R1On
47 r1elssi ⊢A∈⋃R1On→A⊆⋃R1On
48 46 47 syl ⊢Lim⁡rank⁡A→A⊆⋃R1On
49 48 sselda ⊢Lim⁡rank⁡A∧x∈A→x∈⋃R1On
50 ranksnb ⊢x∈⋃R1On→rank⁡x=suc⁡rank⁡x
51 49 50 syl ⊢Lim⁡rank⁡A∧x∈A→rank⁡x=suc⁡rank⁡x
52 rankelb ⊢A∈⋃R1On→x∈A→rank⁡x∈rank⁡A
53 46 52 syl ⊢Lim⁡rank⁡A→x∈A→rank⁡x∈rank⁡A
54 limsuc ⊢Lim⁡rank⁡A→rank⁡x∈rank⁡A↔suc⁡rank⁡x∈rank⁡A
55 53 54 sylibd ⊢Lim⁡rank⁡A→x∈A→suc⁡rank⁡x∈rank⁡A
56 55 imp ⊢Lim⁡rank⁡A∧x∈A→suc⁡rank⁡x∈rank⁡A
57 51 56 eqeltrd ⊢Lim⁡rank⁡A∧x∈A→rank⁡x∈rank⁡A
58 eleq1a ⊢rank⁡x∈rank⁡A→w=rank⁡x→w∈rank⁡A
59 57 58 syl ⊢Lim⁡rank⁡A∧x∈A→w=rank⁡x→w∈rank⁡A
60 59 rexlimdva ⊢Lim⁡rank⁡A→∃x∈Aw=rank⁡x→w∈rank⁡A
61 60 abssdv ⊢Lim⁡rank⁡A→w|∃x∈Aw=rank⁡x⊆rank⁡A
62 vsnex ⊢x∈V
63 62 dfiun2 ⊢⋃x∈Ax=⋃y|∃x∈Ay=x
64 iunid ⊢⋃x∈Ax=A
65 63 64 eqtr3i ⊢⋃y|∃x∈Ay=x=A
66 65 fveq2i ⊢rank⁡⋃y|∃x∈Ay=x=rank⁡A
67 47 sselda ⊢A∈⋃R1On∧x∈A→x∈⋃R1On
68 snwf ⊢x∈⋃R1On→x∈⋃R1On
69 eleq1a ⊢x∈⋃R1On→y=x→y∈⋃R1On
70 67 68 69 3syl ⊢A∈⋃R1On∧x∈A→y=x→y∈⋃R1On
71 70 rexlimdva ⊢A∈⋃R1On→∃x∈Ay=x→y∈⋃R1On
72 71 abssdv ⊢A∈⋃R1On→y|∃x∈Ay=x⊆⋃R1On
73 abrexexg ⊢A∈⋃R1On→y|∃x∈Ay=x∈V
74 eleq1 ⊢z=y|∃x∈Ay=x→z∈⋃R1On↔y|∃x∈Ay=x∈⋃R1On
75 sseq1 ⊢z=y|∃x∈Ay=x→z⊆⋃R1On↔y|∃x∈Ay=x⊆⋃R1On
76 vex ⊢z∈V
77 76 r1elss ⊢z∈⋃R1On↔z⊆⋃R1On
78 74 75 77 vtoclbg ⊢y|∃x∈Ay=x∈V→y|∃x∈Ay=x∈⋃R1On↔y|∃x∈Ay=x⊆⋃R1On
79 73 78 syl ⊢A∈⋃R1On→y|∃x∈Ay=x∈⋃R1On↔y|∃x∈Ay=x⊆⋃R1On
80 72 79 mpbird ⊢A∈⋃R1On→y|∃x∈Ay=x∈⋃R1On
81 rankuni2b ⊢y|∃x∈Ay=x∈⋃R1On→rank⁡⋃y|∃x∈Ay=x=⋃z∈y|∃x∈Ay=xrank⁡z
82 80 81 syl ⊢A∈⋃R1On→rank⁡⋃y|∃x∈Ay=x=⋃z∈y|∃x∈Ay=xrank⁡z
83 66 82 eqtr3id ⊢A∈⋃R1On→rank⁡A=⋃z∈y|∃x∈Ay=xrank⁡z
84 fvex ⊢rank⁡z∈V
85 84 dfiun2 ⊢⋃z∈y|∃x∈Ay=xrank⁡z=⋃w|∃z∈y|∃x∈Ay=xw=rank⁡z
86 fveq2 ⊢z=x→rank⁡z=rank⁡x
87 62 86 abrexco ⊢w|∃z∈y|∃x∈Ay=xw=rank⁡z=w|∃x∈Aw=rank⁡x
88 87 unieqi ⊢⋃w|∃z∈y|∃x∈Ay=xw=rank⁡z=⋃w|∃x∈Aw=rank⁡x
89 85 88 eqtri ⊢⋃z∈y|∃x∈Ay=xrank⁡z=⋃w|∃x∈Aw=rank⁡x
90 83 89 eqtr2di ⊢A∈⋃R1On→⋃w|∃x∈Aw=rank⁡x=rank⁡A
91 46 90 syl ⊢Lim⁡rank⁡A→⋃w|∃x∈Aw=rank⁡x=rank⁡A
92 fvex ⊢rank⁡A∈V
93 92 cfslb ⊢Lim⁡rank⁡A∧w|∃x∈Aw=rank⁡x⊆rank⁡A∧⋃w|∃x∈Aw=rank⁡x=rank⁡A→cf⁡rank⁡A≼w|∃x∈Aw=rank⁡x
94 61 91 93 mpd3an23 ⊢Lim⁡rank⁡A→cf⁡rank⁡A≼w|∃x∈Aw=rank⁡x
95 2fveq3 ⊢y=A→cf⁡rank⁡y=cf⁡rank⁡A
96 breq12 ⊢y=A∧cf⁡rank⁡y=cf⁡rank⁡A→y≺cf⁡rank⁡y↔A≺cf⁡rank⁡A
97 95 96 mpdan ⊢y=A→y≺cf⁡rank⁡y↔A≺cf⁡rank⁡A
98 rexeq ⊢y=A→∃x∈yw=rank⁡x↔∃x∈Aw=rank⁡x
99 98 abbidv ⊢y=A→w|∃x∈yw=rank⁡x=w|∃x∈Aw=rank⁡x
100 breq12 ⊢w|∃x∈yw=rank⁡x=w|∃x∈Aw=rank⁡x∧y=A→w|∃x∈yw=rank⁡x≼y↔w|∃x∈Aw=rank⁡x≼A
101 99 100 mpancom ⊢y=A→w|∃x∈yw=rank⁡x≼y↔w|∃x∈Aw=rank⁡x≼A
102 97 101 imbi12d ⊢y=A→y≺cf⁡rank⁡y→w|∃x∈yw=rank⁡x≼y↔A≺cf⁡rank⁡A→w|∃x∈Aw=rank⁡x≼A
103 eqid ⊢x∈y⟼rank⁡x=x∈y⟼rank⁡x
104 103 rnmpt ⊢ran⁡x∈y⟼rank⁡x=w|∃x∈yw=rank⁡x
105 cfon ⊢cf⁡rank⁡y∈On
106 sdomdom ⊢y≺cf⁡rank⁡y→y≼cf⁡rank⁡y
107 ondomen ⊢cf⁡rank⁡y∈On∧y≼cf⁡rank⁡y→y∈dom⁡card
108 105 106 107 sylancr ⊢y≺cf⁡rank⁡y→y∈dom⁡card
109 fvex ⊢rank⁡x∈V
110 109 103 fnmpti ⊢x∈y⟼rank⁡xFny
111 dffn4 ⊢x∈y⟼rank⁡xFny↔x∈y⟼rank⁡x:y⟶ontoran⁡x∈y⟼rank⁡x
112 110 111 mpbi ⊢x∈y⟼rank⁡x:y⟶ontoran⁡x∈y⟼rank⁡x
113 fodomnum ⊢y∈dom⁡card→x∈y⟼rank⁡x:y⟶ontoran⁡x∈y⟼rank⁡x→ran⁡x∈y⟼rank⁡x≼y
114 108 112 113 mpisyl ⊢y≺cf⁡rank⁡y→ran⁡x∈y⟼rank⁡x≼y
115 104 114 eqbrtrrid ⊢y≺cf⁡rank⁡y→w|∃x∈yw=rank⁡x≼y
116 102 115 vtoclg ⊢A∈⋃R1On→A≺cf⁡rank⁡A→w|∃x∈Aw=rank⁡x≼A
117 46 116 syl ⊢Lim⁡rank⁡A→A≺cf⁡rank⁡A→w|∃x∈Aw=rank⁡x≼A
118 domtr ⊢cf⁡rank⁡A≼w|∃x∈Aw=rank⁡x∧w|∃x∈Aw=rank⁡x≼A→cf⁡rank⁡A≼A
119 118 40 syl ⊢cf⁡rank⁡A≼w|∃x∈Aw=rank⁡x∧w|∃x∈Aw=rank⁡x≼A→¬A≺cf⁡rank⁡A
120 94 117 119 syl6an ⊢Lim⁡rank⁡A→A≺cf⁡rank⁡A→¬A≺cf⁡rank⁡A
121 120 pm2.01d ⊢Lim⁡rank⁡A→¬A≺cf⁡rank⁡A
122 121 adantl ⊢rank⁡A∈V∧Lim⁡rank⁡A→¬A≺cf⁡rank⁡A
123 9 41 122 3jaoi ⊢rank⁡A=∅∨∃x∈Onrank⁡A=suc⁡x∨rank⁡A∈V∧Lim⁡rank⁡A→¬A≺cf⁡rank⁡A
124 3 123 ax-mp ⊢¬A≺cf⁡rank⁡A