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 syl6eq 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 fndm R1 Fn On dom R1 = On
20 18 19 ax-mp dom R1 = On
21 17 20 eleqtrri dom R1
22 rankonid dom R1 rank =
23 21 22 mpbi rank =
24 16 23 syl6eq A = rank A =
25 24 necon3i rank A A
26 rankvaln ¬ A R1 On rank A =
27 26 necon1ai rank A A R1 On
28 breq2 y = A 1 𝑜 y 1 𝑜 A
29 neeq1 y = A y A
30 0sdom1dom y 1 𝑜 y
31 vex y V
32 31 0sdom y y
33 30 32 bitr3i 1 𝑜 y y
34 28 29 33 vtoclbg A R1 On 1 𝑜 A A
35 27 34 syl rank A 1 𝑜 A A
36 25 35 mpbird rank A 1 𝑜 A
37 15 36 syl rank A = suc x 1 𝑜 A
38 37 adantl x On rank A = suc x 1 𝑜 A
39 12 38 eqbrtrd x On rank A = suc x cf rank A A
40 39 rexlimiva x On rank A = suc x cf rank A A
41 domnsym cf rank A A ¬ A cf rank A
42 40 41 syl x On rank A = suc x ¬ A cf rank A
43 nlim0 ¬ Lim
44 limeq rank A = Lim rank A Lim
45 43 44 mtbiri rank A = ¬ Lim rank A
46 26 45 syl ¬ A R1 On ¬ Lim rank A
47 46 con4i Lim rank A A R1 On
48 r1elssi A R1 On A R1 On
49 47 48 syl Lim rank A A R1 On
50 49 sselda Lim rank A x A x R1 On
51 ranksnb x R1 On rank x = suc rank x
52 50 51 syl Lim rank A x A rank x = suc rank x
53 rankelb A R1 On x A rank x rank A
54 47 53 syl Lim rank A x A rank x rank A
55 limsuc Lim rank A rank x rank A suc rank x rank A
56 54 55 sylibd Lim rank A x A suc rank x rank A
57 56 imp Lim rank A x A suc rank x rank A
58 52 57 eqeltrd Lim rank A x A rank x rank A
59 eleq1a rank x rank A w = rank x w rank A
60 58 59 syl Lim rank A x A w = rank x w rank A
61 60 rexlimdva Lim rank A x A w = rank x w rank A
62 61 abssdv Lim rank A w | x A w = rank x rank A
63 snex x V
64 63 dfiun2 x A x = y | x A y = x
65 iunid x A x = A
66 64 65 eqtr3i y | x A y = x = A
67 66 fveq2i rank y | x A y = x = rank A
68 48 sselda A R1 On x A x R1 On
69 snwf x R1 On x R1 On
70 eleq1a x R1 On y = x y R1 On
71 68 69 70 3syl A R1 On x A y = x y R1 On
72 71 rexlimdva A R1 On x A y = x y R1 On
73 72 abssdv A R1 On y | x A y = x R1 On
74 abrexexg A R1 On y | x A y = x V
75 eleq1 z = y | x A y = x z R1 On y | x A y = x R1 On
76 sseq1 z = y | x A y = x z R1 On y | x A y = x R1 On
77 vex z V
78 77 r1elss z R1 On z R1 On
79 75 76 78 vtoclbg y | x A y = x V y | x A y = x R1 On y | x A y = x R1 On
80 74 79 syl A R1 On y | x A y = x R1 On y | x A y = x R1 On
81 73 80 mpbird A R1 On y | x A y = x R1 On
82 rankuni2b y | x A y = x R1 On rank y | x A y = x = z y | x A y = x rank z
83 81 82 syl A R1 On rank y | x A y = x = z y | x A y = x rank z
84 67 83 syl5eqr A R1 On rank A = z y | x A y = x rank z
85 fvex rank z V
86 85 dfiun2 z y | x A y = x rank z = w | z y | x A y = x w = rank z
87 fveq2 z = x rank z = rank x
88 63 87 abrexco w | z y | x A y = x w = rank z = w | x A w = rank x
89 88 unieqi w | z y | x A y = x w = rank z = w | x A w = rank x
90 86 89 eqtri z y | x A y = x rank z = w | x A w = rank x
91 84 90 syl6req A R1 On w | x A w = rank x = rank A
92 47 91 syl Lim rank A w | x A w = rank x = rank A
93 fvex rank A V
94 93 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
95 62 92 94 mpd3an23 Lim rank A cf rank A w | x A w = rank x
96 2fveq3 y = A cf rank y = cf rank A
97 breq12 y = A cf rank y = cf rank A y cf rank y A cf rank A
98 96 97 mpdan y = A y cf rank y A cf rank A
99 rexeq y = A x y w = rank x x A w = rank x
100 99 abbidv y = A w | x y w = rank x = w | x A w = rank x
101 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
102 100 101 mpancom y = A w | x y w = rank x y w | x A w = rank x A
103 98 102 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
104 eqid x y rank x = x y rank x
105 104 rnmpt ran x y rank x = w | x y w = rank x
106 cfon cf rank y On
107 sdomdom y cf rank y y cf rank y
108 ondomen cf rank y On y cf rank y y dom card
109 106 107 108 sylancr y cf rank y y dom card
110 fvex rank x V
111 110 104 fnmpti x y rank x Fn y
112 dffn4 x y rank x Fn y x y rank x : y onto ran x y rank x
113 111 112 mpbi x y rank x : y onto ran x y rank x
114 fodomnum y dom card x y rank x : y onto ran x y rank x ran x y rank x y
115 109 113 114 mpisyl y cf rank y ran x y rank x y
116 105 115 eqbrtrrid y cf rank y w | x y w = rank x y
117 103 116 vtoclg A R1 On A cf rank A w | x A w = rank x A
118 47 117 syl Lim rank A A cf rank A w | x A w = rank x A
119 domtr cf rank A w | x A w = rank x w | x A w = rank x A cf rank A A
120 119 41 syl cf rank A w | x A w = rank x w | x A w = rank x A ¬ A cf rank A
121 95 118 120 syl6an Lim rank A A cf rank A ¬ A cf rank A
122 121 pm2.01d Lim rank A ¬ A cf rank A
123 122 adantl rank A V Lim rank A ¬ A cf rank A
124 9 42 123 3jaoi rank A = x On rank A = suc x rank A V Lim rank A ¬ A cf rank A
125 3 124 ax-mp ¬ A cf rank A