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 On rank A = suc x rank A V Lim rank A
3 1 2 mpbi rank A = x On rank 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 R1 Fn On
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 R1 On rank A =
26 25 necon1ai rank A A R1 On
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 R1 On 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 On rank A = suc x cf rank A A
40 domnsym cf rank A A ¬ A cf rank A
41 39 40 syl x On rank 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 R1 On ¬ Lim rank A
46 45 con4i Lim rank A A R1 On
47 r1elssi A R1 On A R1 On
48 46 47 syl Lim rank A A R1 On
49 48 sselda Lim rank A x A x R1 On
50 ranksnb x R1 On rank x = suc rank x
51 49 50 syl Lim rank A x A rank x = suc rank x
52 rankelb A R1 On 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 A w = rank x w rank A
61 60 abssdv Lim rank A w | x A w = rank x rank A
62 snex x V
63 62 dfiun2 x A x = y | x A y = x
64 iunid x A x = A
65 63 64 eqtr3i y | x A y = x = A
66 65 fveq2i rank y | x A y = x = rank A
67 47 sselda A R1 On x A x R1 On
68 snwf x R1 On x R1 On
69 eleq1a x R1 On y = x y R1 On
70 67 68 69 3syl A R1 On x A y = x y R1 On
71 70 rexlimdva A R1 On x A y = x y R1 On
72 71 abssdv A R1 On y | x A y = x R1 On
73 abrexexg A R1 On y | x A y = x V
74 eleq1 z = y | x A y = x z R1 On y | x A y = x R1 On
75 sseq1 z = y | x A y = x z R1 On y | x A y = x R1 On
76 vex z V
77 76 r1elss z R1 On z R1 On
78 74 75 77 vtoclbg y | x A y = x V y | x A y = x R1 On y | x A y = x R1 On
79 73 78 syl A R1 On y | x A y = x R1 On y | x A y = x R1 On
80 72 79 mpbird A R1 On y | x A y = x R1 On
81 rankuni2b y | x A y = x R1 On rank y | x A y = x = z y | x A y = x rank z
82 80 81 syl A R1 On rank y | x A y = x = z y | x A y = x rank z
83 66 82 eqtr3id A R1 On rank A = z y | x A y = x rank z
84 fvex rank z V
85 84 dfiun2 z y | x A y = x rank z = w | z y | x A y = x w = rank z
86 fveq2 z = x rank z = rank x
87 62 86 abrexco w | z y | x A y = x w = rank z = w | x A w = rank x
88 87 unieqi w | z y | x A y = x w = rank z = w | x A w = rank x
89 85 88 eqtri z y | x A y = x rank z = w | x A w = rank x
90 83 89 eqtr2di A R1 On w | x A w = rank x = rank A
91 46 90 syl Lim rank A w | x A w = rank x = rank A
92 fvex rank A V
93 92 cfslb Lim rank A w | x A w = rank x rank A w | x A w = rank x = rank A cf rank A w | x A w = rank x
94 61 91 93 mpd3an23 Lim rank A cf rank A w | x A w = 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 y w = rank x x A w = rank x
99 98 abbidv y = A w | x y w = rank x = w | x A w = rank x
100 breq12 w | x y w = rank x = w | x A w = rank x y = A w | x y w = rank x y w | x A w = rank x A
101 99 100 mpancom y = A w | x y w = rank x y w | x A w = rank x A
102 97 101 imbi12d y = A y cf rank y w | x y w = rank x y A cf rank A w | x A w = rank x A
103 eqid x y rank x = x y rank x
104 103 rnmpt ran x y rank x = w | x y w = 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 x Fn y
111 dffn4 x y rank x Fn y x y rank x : y onto ran x y rank x
112 110 111 mpbi x y rank x : y onto ran x y rank x
113 fodomnum y dom card x y rank x : y onto ran 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 y w = rank x y
116 102 115 vtoclg A R1 On A cf rank A w | x A w = rank x A
117 46 116 syl Lim rank A A cf rank A w | x A w = rank x A
118 domtr cf rank A w | x A w = rank x w | x A w = rank x A cf rank A A
119 118 40 syl cf rank A w | x A w = rank x w | x A w = 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 On rank A = suc x rank A V Lim rank A ¬ A cf rank A
124 3 123 ax-mp ¬ A cf rank A