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 ) e. On
2 onzsl 
 |-  ( ( rank ` A ) e. On <-> ( ( rank ` A ) = (/) \/ E. x e. On ( rank ` A ) = suc x \/ ( ( rank ` A ) e. _V /\ Lim ( rank ` A ) ) ) )
3 1 2 mpbi 
 |-  ( ( rank ` A ) = (/) \/ E. x e. On ( rank ` A ) = suc x \/ ( ( rank ` A ) e. _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 e. On -> ( cf ` suc x ) = 1o )
12 10 11 sylan9eqr 
 |-  ( ( x e. On /\ ( rank ` A ) = suc x ) -> ( cf ` ( rank ` A ) ) = 1o )
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 
 |-  (/) e. On
18 r1fnon 
 |-  R1 Fn On
19 18 fndmi 
 |-  dom R1 = On
20 17 19 eleqtrri 
 |-  (/) e. dom R1
21 rankonid 
 |-  ( (/) e. dom R1 <-> ( rank ` (/) ) = (/) )
22 20 21 mpbi 
 |-  ( rank ` (/) ) = (/)
23 16 22 eqtrdi 
 |-  ( A = (/) -> ( rank ` A ) = (/) )
24 23 necon3i 
 |-  ( ( rank ` A ) =/= (/) -> A =/= (/) )
25 rankvaln 
 |-  ( -. A e. U. ( R1 " On ) -> ( rank ` A ) = (/) )
26 25 necon1ai 
 |-  ( ( rank ` A ) =/= (/) -> A e. U. ( R1 " On ) )
27 breq2 
 |-  ( y = A -> ( 1o ~<_ y <-> 1o ~<_ A ) )
28 neeq1 
 |-  ( y = A -> ( y =/= (/) <-> A =/= (/) ) )
29 0sdom1dom 
 |-  ( (/) ~< y <-> 1o ~<_ y )
30 vex 
 |-  y e. _V
31 30 0sdom 
 |-  ( (/) ~< y <-> y =/= (/) )
32 29 31 bitr3i 
 |-  ( 1o ~<_ y <-> y =/= (/) )
33 27 28 32 vtoclbg 
 |-  ( A e. U. ( R1 " On ) -> ( 1o ~<_ A <-> A =/= (/) ) )
34 26 33 syl 
 |-  ( ( rank ` A ) =/= (/) -> ( 1o ~<_ A <-> A =/= (/) ) )
35 24 34 mpbird 
 |-  ( ( rank ` A ) =/= (/) -> 1o ~<_ A )
36 15 35 syl 
 |-  ( ( rank ` A ) = suc x -> 1o ~<_ A )
37 36 adantl 
 |-  ( ( x e. On /\ ( rank ` A ) = suc x ) -> 1o ~<_ A )
38 12 37 eqbrtrd 
 |-  ( ( x e. On /\ ( rank ` A ) = suc x ) -> ( cf ` ( rank ` A ) ) ~<_ A )
39 38 rexlimiva 
 |-  ( E. x e. On ( rank ` A ) = suc x -> ( cf ` ( rank ` A ) ) ~<_ A )
40 domnsym 
 |-  ( ( cf ` ( rank ` A ) ) ~<_ A -> -. A ~< ( cf ` ( rank ` A ) ) )
41 39 40 syl 
 |-  ( E. x e. 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 e. U. ( R1 " On ) -> -. Lim ( rank ` A ) )
46 45 con4i 
 |-  ( Lim ( rank ` A ) -> A e. U. ( R1 " On ) )
47 r1elssi 
 |-  ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )
48 46 47 syl 
 |-  ( Lim ( rank ` A ) -> A C_ U. ( R1 " On ) )
49 48 sselda 
 |-  ( ( Lim ( rank ` A ) /\ x e. A ) -> x e. U. ( R1 " On ) )
50 ranksnb 
 |-  ( x e. U. ( R1 " On ) -> ( rank ` { x } ) = suc ( rank ` x ) )
51 49 50 syl 
 |-  ( ( Lim ( rank ` A ) /\ x e. A ) -> ( rank ` { x } ) = suc ( rank ` x ) )
52 rankelb 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
53 46 52 syl 
 |-  ( Lim ( rank ` A ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
54 limsuc 
 |-  ( Lim ( rank ` A ) -> ( ( rank ` x ) e. ( rank ` A ) <-> suc ( rank ` x ) e. ( rank ` A ) ) )
55 53 54 sylibd 
 |-  ( Lim ( rank ` A ) -> ( x e. A -> suc ( rank ` x ) e. ( rank ` A ) ) )
56 55 imp 
 |-  ( ( Lim ( rank ` A ) /\ x e. A ) -> suc ( rank ` x ) e. ( rank ` A ) )
57 51 56 eqeltrd 
 |-  ( ( Lim ( rank ` A ) /\ x e. A ) -> ( rank ` { x } ) e. ( rank ` A ) )
58 eleq1a 
 |-  ( ( rank ` { x } ) e. ( rank ` A ) -> ( w = ( rank ` { x } ) -> w e. ( rank ` A ) ) )
59 57 58 syl 
 |-  ( ( Lim ( rank ` A ) /\ x e. A ) -> ( w = ( rank ` { x } ) -> w e. ( rank ` A ) ) )
60 59 rexlimdva 
 |-  ( Lim ( rank ` A ) -> ( E. x e. A w = ( rank ` { x } ) -> w e. ( rank ` A ) ) )
61 60 abssdv 
 |-  ( Lim ( rank ` A ) -> { w | E. x e. A w = ( rank ` { x } ) } C_ ( rank ` A ) )
62 vsnex 
 |-  { x } e. _V
63 62 dfiun2 
 |-  U_ x e. A { x } = U. { y | E. x e. A y = { x } }
64 iunid 
 |-  U_ x e. A { x } = A
65 63 64 eqtr3i 
 |-  U. { y | E. x e. A y = { x } } = A
66 65 fveq2i 
 |-  ( rank ` U. { y | E. x e. A y = { x } } ) = ( rank ` A )
67 47 sselda 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. A ) -> x e. U. ( R1 " On ) )
68 snwf 
 |-  ( x e. U. ( R1 " On ) -> { x } e. U. ( R1 " On ) )
69 eleq1a 
 |-  ( { x } e. U. ( R1 " On ) -> ( y = { x } -> y e. U. ( R1 " On ) ) )
70 67 68 69 3syl 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. A ) -> ( y = { x } -> y e. U. ( R1 " On ) ) )
71 70 rexlimdva 
 |-  ( A e. U. ( R1 " On ) -> ( E. x e. A y = { x } -> y e. U. ( R1 " On ) ) )
72 71 abssdv 
 |-  ( A e. U. ( R1 " On ) -> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) )
73 abrexexg 
 |-  ( A e. U. ( R1 " On ) -> { y | E. x e. A y = { x } } e. _V )
74 eleq1 
 |-  ( z = { y | E. x e. A y = { x } } -> ( z e. U. ( R1 " On ) <-> { y | E. x e. A y = { x } } e. U. ( R1 " On ) ) )
75 sseq1 
 |-  ( z = { y | E. x e. A y = { x } } -> ( z C_ U. ( R1 " On ) <-> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) ) )
76 vex 
 |-  z e. _V
77 76 r1elss 
 |-  ( z e. U. ( R1 " On ) <-> z C_ U. ( R1 " On ) )
78 74 75 77 vtoclbg 
 |-  ( { y | E. x e. A y = { x } } e. _V -> ( { y | E. x e. A y = { x } } e. U. ( R1 " On ) <-> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) ) )
79 73 78 syl 
 |-  ( A e. U. ( R1 " On ) -> ( { y | E. x e. A y = { x } } e. U. ( R1 " On ) <-> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) ) )
80 72 79 mpbird 
 |-  ( A e. U. ( R1 " On ) -> { y | E. x e. A y = { x } } e. U. ( R1 " On ) )
81 rankuni2b 
 |-  ( { y | E. x e. A y = { x } } e. U. ( R1 " On ) -> ( rank ` U. { y | E. x e. A y = { x } } ) = U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) )
82 80 81 syl 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` U. { y | E. x e. A y = { x } } ) = U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) )
83 66 82 eqtr3id 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) )
84 fvex 
 |-  ( rank ` z ) e. _V
85 84 dfiun2 
 |-  U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) = U. { w | E. z e. { y | E. x e. A y = { x } } w = ( rank ` z ) }
86 fveq2 
 |-  ( z = { x } -> ( rank ` z ) = ( rank ` { x } ) )
87 62 86 abrexco 
 |-  { w | E. z e. { y | E. x e. A y = { x } } w = ( rank ` z ) } = { w | E. x e. A w = ( rank ` { x } ) }
88 87 unieqi 
 |-  U. { w | E. z e. { y | E. x e. A y = { x } } w = ( rank ` z ) } = U. { w | E. x e. A w = ( rank ` { x } ) }
89 85 88 eqtri 
 |-  U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) = U. { w | E. x e. A w = ( rank ` { x } ) }
90 83 89 eqtr2di 
 |-  ( A e. U. ( R1 " On ) -> U. { w | E. x e. A w = ( rank ` { x } ) } = ( rank ` A ) )
91 46 90 syl 
 |-  ( Lim ( rank ` A ) -> U. { w | E. x e. A w = ( rank ` { x } ) } = ( rank ` A ) )
92 fvex 
 |-  ( rank ` A ) e. _V
93 92 cfslb 
 |-  ( ( Lim ( rank ` A ) /\ { w | E. x e. A w = ( rank ` { x } ) } C_ ( rank ` A ) /\ U. { w | E. x e. A w = ( rank ` { x } ) } = ( rank ` A ) ) -> ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. A w = ( rank ` { x } ) } )
94 61 91 93 mpd3an23 
 |-  ( Lim ( rank ` A ) -> ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. 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 -> ( E. x e. y w = ( rank ` { x } ) <-> E. x e. A w = ( rank ` { x } ) ) )
99 98 abbidv 
 |-  ( y = A -> { w | E. x e. y w = ( rank ` { x } ) } = { w | E. x e. A w = ( rank ` { x } ) } )
100 breq12 
 |-  ( ( { w | E. x e. y w = ( rank ` { x } ) } = { w | E. x e. A w = ( rank ` { x } ) } /\ y = A ) -> ( { w | E. x e. y w = ( rank ` { x } ) } ~<_ y <-> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
101 99 100 mpancom 
 |-  ( y = A -> ( { w | E. x e. y w = ( rank ` { x } ) } ~<_ y <-> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
102 97 101 imbi12d 
 |-  ( y = A -> ( ( y ~< ( cf ` ( rank ` y ) ) -> { w | E. x e. y w = ( rank ` { x } ) } ~<_ y ) <-> ( A ~< ( cf ` ( rank ` A ) ) -> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) ) )
103 eqid 
 |-  ( x e. y |-> ( rank ` { x } ) ) = ( x e. y |-> ( rank ` { x } ) )
104 103 rnmpt 
 |-  ran ( x e. y |-> ( rank ` { x } ) ) = { w | E. x e. y w = ( rank ` { x } ) }
105 cfon 
 |-  ( cf ` ( rank ` y ) ) e. On
106 sdomdom 
 |-  ( y ~< ( cf ` ( rank ` y ) ) -> y ~<_ ( cf ` ( rank ` y ) ) )
107 ondomen 
 |-  ( ( ( cf ` ( rank ` y ) ) e. On /\ y ~<_ ( cf ` ( rank ` y ) ) ) -> y e. dom card )
108 105 106 107 sylancr 
 |-  ( y ~< ( cf ` ( rank ` y ) ) -> y e. dom card )
109 fvex 
 |-  ( rank ` { x } ) e. _V
110 109 103 fnmpti 
 |-  ( x e. y |-> ( rank ` { x } ) ) Fn y
111 dffn4 
 |-  ( ( x e. y |-> ( rank ` { x } ) ) Fn y <-> ( x e. y |-> ( rank ` { x } ) ) : y -onto-> ran ( x e. y |-> ( rank ` { x } ) ) )
112 110 111 mpbi 
 |-  ( x e. y |-> ( rank ` { x } ) ) : y -onto-> ran ( x e. y |-> ( rank ` { x } ) )
113 fodomnum 
 |-  ( y e. dom card -> ( ( x e. y |-> ( rank ` { x } ) ) : y -onto-> ran ( x e. y |-> ( rank ` { x } ) ) -> ran ( x e. y |-> ( rank ` { x } ) ) ~<_ y ) )
114 108 112 113 mpisyl 
 |-  ( y ~< ( cf ` ( rank ` y ) ) -> ran ( x e. y |-> ( rank ` { x } ) ) ~<_ y )
115 104 114 eqbrtrrid 
 |-  ( y ~< ( cf ` ( rank ` y ) ) -> { w | E. x e. y w = ( rank ` { x } ) } ~<_ y )
116 102 115 vtoclg 
 |-  ( A e. U. ( R1 " On ) -> ( A ~< ( cf ` ( rank ` A ) ) -> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
117 46 116 syl 
 |-  ( Lim ( rank ` A ) -> ( A ~< ( cf ` ( rank ` A ) ) -> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
118 domtr 
 |-  ( ( ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. A w = ( rank ` { x } ) } /\ { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) -> ( cf ` ( rank ` A ) ) ~<_ A )
119 118 40 syl 
 |-  ( ( ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. A w = ( rank ` { x } ) } /\ { w | E. x e. 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 ) e. _V /\ Lim ( rank ` A ) ) -> -. A ~< ( cf ` ( rank ` A ) ) )
123 9 41 122 3jaoi 
 |-  ( ( ( rank ` A ) = (/) \/ E. x e. On ( rank ` A ) = suc x \/ ( ( rank ` A ) e. _V /\ Lim ( rank ` A ) ) ) -> -. A ~< ( cf ` ( rank ` A ) ) )
124 3 123 ax-mp 
 |-  -. A ~< ( cf ` ( rank ` A ) )