Metamath Proof Explorer

Theorem cfflb

Description: If there is a cofinal map from B to A , then B is at least ( cfA ) . This theorem and cff1 motivate the picture of ( cfA ) as the greatest lower bound of the domain of cofinal maps into A . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion cfflb 
|- ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( cf ` A ) C_ B ) )

Proof

Step Hyp Ref Expression
1 frn 
 |-  ( f : B --> A -> ran f C_ A )
2 1 adantr 
 |-  ( ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ran f C_ A )
3 ffn 
 |-  ( f : B --> A -> f Fn B )
4 fnfvelrn 
 |-  ( ( f Fn B /\ w e. B ) -> ( f ` w ) e. ran f )
5 3 4 sylan 
 |-  ( ( f : B --> A /\ w e. B ) -> ( f ` w ) e. ran f )
6 sseq2 
 |-  ( s = ( f ` w ) -> ( z C_ s <-> z C_ ( f ` w ) ) )
7 6 rspcev 
 |-  ( ( ( f ` w ) e. ran f /\ z C_ ( f ` w ) ) -> E. s e. ran f z C_ s )
8 5 7 sylan 
 |-  ( ( ( f : B --> A /\ w e. B ) /\ z C_ ( f ` w ) ) -> E. s e. ran f z C_ s )
9 8 rexlimdva2 
 |-  ( f : B --> A -> ( E. w e. B z C_ ( f ` w ) -> E. s e. ran f z C_ s ) )
10 9 ralimdv 
 |-  ( f : B --> A -> ( A. z e. A E. w e. B z C_ ( f ` w ) -> A. z e. A E. s e. ran f z C_ s ) )
11 10 imp 
 |-  ( ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> A. z e. A E. s e. ran f z C_ s )
12 2 11 jca 
 |-  ( ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) )
13 fvex 
 |-  ( card ` ran f ) e. _V
14 cfval 
 |-  ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
15 14 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
16 15 3ad2ant2 
 |-  ( ( x = ( card ` ran f ) /\ ( A e. On /\ B e. On ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
17 vex 
 |-  f e. _V
18 17 rnex 
 |-  ran f e. _V
19 fveq2 
 |-  ( y = ran f -> ( card ` y ) = ( card ` ran f ) )
20 19 eqeq2d 
 |-  ( y = ran f -> ( x = ( card ` y ) <-> x = ( card ` ran f ) ) )
21 sseq1 
 |-  ( y = ran f -> ( y C_ A <-> ran f C_ A ) )
22 rexeq 
 |-  ( y = ran f -> ( E. s e. y z C_ s <-> E. s e. ran f z C_ s ) )
23 22 ralbidv 
 |-  ( y = ran f -> ( A. z e. A E. s e. y z C_ s <-> A. z e. A E. s e. ran f z C_ s ) )
24 21 23 anbi12d 
 |-  ( y = ran f -> ( ( y C_ A /\ A. z e. A E. s e. y z C_ s ) <-> ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) )
25 20 24 anbi12d 
 |-  ( y = ran f -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) <-> ( x = ( card ` ran f ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) ) )
26 18 25 spcev 
 |-  ( ( x = ( card ` ran f ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) )
27 abid 
 |-  ( x e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } <-> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) )
28 26 27 sylibr 
 |-  ( ( x = ( card ` ran f ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> x e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
29 intss1 
 |-  ( x e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } C_ x )
30 28 29 syl 
 |-  ( ( x = ( card ` ran f ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } C_ x )
31 30 3adant2 
 |-  ( ( x = ( card ` ran f ) /\ ( A e. On /\ B e. On ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } C_ x )
32 16 31 eqsstrd 
 |-  ( ( x = ( card ` ran f ) /\ ( A e. On /\ B e. On ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> ( cf ` A ) C_ x )
33 32 3expib 
 |-  ( x = ( card ` ran f ) -> ( ( ( A e. On /\ B e. On ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> ( cf ` A ) C_ x ) )
34 sseq2 
 |-  ( x = ( card ` ran f ) -> ( ( cf ` A ) C_ x <-> ( cf ` A ) C_ ( card ` ran f ) ) )
35 33 34 sylibd 
 |-  ( x = ( card ` ran f ) -> ( ( ( A e. On /\ B e. On ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> ( cf ` A ) C_ ( card ` ran f ) ) )
36 13 35 vtocle 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( ran f C_ A /\ A. z e. A E. s e. ran f z C_ s ) ) -> ( cf ` A ) C_ ( card ` ran f ) )
37 12 36 sylan2 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( cf ` A ) C_ ( card ` ran f ) )
38 cardidm 
 |-  ( card ` ( card ` ran f ) ) = ( card ` ran f )
39 onss 
 |-  ( A e. On -> A C_ On )
40 1 39 sylan9ssr 
 |-  ( ( A e. On /\ f : B --> A ) -> ran f C_ On )
41 40 3adant2 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ran f C_ On )
42 onssnum 
 |-  ( ( ran f e. _V /\ ran f C_ On ) -> ran f e. dom card )
43 18 41 42 sylancr 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ran f e. dom card )
44 cardid2 
 |-  ( ran f e. dom card -> ( card ` ran f ) ~~ ran f )
45 43 44 syl 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ( card ` ran f ) ~~ ran f )
46 onenon 
 |-  ( B e. On -> B e. dom card )
47 dffn4 
 |-  ( f Fn B <-> f : B -onto-> ran f )
48 3 47 sylib 
 |-  ( f : B --> A -> f : B -onto-> ran f )
49 fodomnum 
 |-  ( B e. dom card -> ( f : B -onto-> ran f -> ran f ~<_ B ) )
50 46 48 49 syl2im 
 |-  ( B e. On -> ( f : B --> A -> ran f ~<_ B ) )
51 50 imp 
 |-  ( ( B e. On /\ f : B --> A ) -> ran f ~<_ B )
52 51 3adant1 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ran f ~<_ B )
53 endomtr 
 |-  ( ( ( card ` ran f ) ~~ ran f /\ ran f ~<_ B ) -> ( card ` ran f ) ~<_ B )
54 45 52 53 syl2anc 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ( card ` ran f ) ~<_ B )
55 cardon 
 |-  ( card ` ran f ) e. On
56 onenon 
 |-  ( ( card ` ran f ) e. On -> ( card ` ran f ) e. dom card )
57 55 56 ax-mp 
 |-  ( card ` ran f ) e. dom card
58 carddom2 
 |-  ( ( ( card ` ran f ) e. dom card /\ B e. dom card ) -> ( ( card ` ( card ` ran f ) ) C_ ( card ` B ) <-> ( card ` ran f ) ~<_ B ) )
59 57 46 58 sylancr 
 |-  ( B e. On -> ( ( card ` ( card ` ran f ) ) C_ ( card ` B ) <-> ( card ` ran f ) ~<_ B ) )
60 59 3ad2ant2 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ( ( card ` ( card ` ran f ) ) C_ ( card ` B ) <-> ( card ` ran f ) ~<_ B ) )
61 54 60 mpbird 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ( card ` ( card ` ran f ) ) C_ ( card ` B ) )
62 cardonle 
 |-  ( B e. On -> ( card ` B ) C_ B )
63 62 3ad2ant2 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ( card ` B ) C_ B )
64 61 63 sstrd 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ( card ` ( card ` ran f ) ) C_ B )
65 38 64 eqsstrrid 
 |-  ( ( A e. On /\ B e. On /\ f : B --> A ) -> ( card ` ran f ) C_ B )
66 65 3expa 
 |-  ( ( ( A e. On /\ B e. On ) /\ f : B --> A ) -> ( card ` ran f ) C_ B )
67 66 adantrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( card ` ran f ) C_ B )
68 37 67 sstrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( cf ` A ) C_ B )
69 68 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( cf ` A ) C_ B ) )
70 69 exlimdv 
 |-  ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( cf ` A ) C_ B ) )