Metamath Proof Explorer

Theorem cfcof

Description: If there is a cofinal map from A to B , then they have the same cofinality. This was used as Definition 11.1 of TakeutiZaring p. 100, who defines an equivalence relation cof ( A , B ) and defines our cf ( B ) as the minimum B such that cof ( A , B ) . (Contributed by Mario Carneiro, 20-Mar-2013)

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

Proof

Step Hyp Ref Expression
1 cfcoflem 
 |-  ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( cf ` A ) C_ ( cf ` B ) ) )
2 1 imp 
 |-  ( ( ( A e. On /\ B e. On ) /\ E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( cf ` A ) C_ ( cf ` B ) )
3 cff1 
 |-  ( A e. On -> E. g ( g : ( cf ` A ) -1-1-> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) )
4 f1f 
 |-  ( g : ( cf ` A ) -1-1-> A -> g : ( cf ` A ) --> A )
5 4 anim1i 
 |-  ( ( g : ( cf ` A ) -1-1-> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) -> ( g : ( cf ` A ) --> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) )
6 5 eximi 
 |-  ( E. g ( g : ( cf ` A ) -1-1-> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) -> E. g ( g : ( cf ` A ) --> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) )
7 3 6 syl 
 |-  ( A e. On -> E. g ( g : ( cf ` A ) --> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) )
8 eqid 
 |-  ( y e. ( cf ` A ) |-> |^| { v e. B | ( g ` y ) C_ ( f ` v ) } ) = ( y e. ( cf ` A ) |-> |^| { v e. B | ( g ` y ) C_ ( f ` v ) } )
9 8 coftr 
 |-  ( E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( E. g ( g : ( cf ` A ) --> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) -> E. h ( h : ( cf ` A ) --> B /\ A. r e. B E. t e. ( cf ` A ) r C_ ( h ` t ) ) ) )
10 7 9 syl5com 
 |-  ( A e. On -> ( E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> E. h ( h : ( cf ` A ) --> B /\ A. r e. B E. t e. ( cf ` A ) r C_ ( h ` t ) ) ) )
11 eloni 
 |-  ( B e. On -> Ord B )
12 cfon 
 |-  ( cf ` A ) e. On
13 eqid 
 |-  { x e. ( cf ` A ) | A. t e. x ( h ` t ) e. ( h ` x ) } = { x e. ( cf ` A ) | A. t e. x ( h ` t ) e. ( h ` x ) }
14 eqid 
 |-  |^| { c e. ( cf ` A ) | r C_ ( h ` c ) } = |^| { c e. ( cf ` A ) | r C_ ( h ` c ) }
15 eqid 
 |-  OrdIso ( _E , { x e. ( cf ` A ) | A. t e. x ( h ` t ) e. ( h ` x ) } ) = OrdIso ( _E , { x e. ( cf ` A ) | A. t e. x ( h ` t ) e. ( h ` x ) } )
16 13 14 15 cofsmo 
 |-  ( ( Ord B /\ ( cf ` A ) e. On ) -> ( E. h ( h : ( cf ` A ) --> B /\ A. r e. B E. t e. ( cf ` A ) r C_ ( h ` t ) ) -> E. c e. suc ( cf ` A ) E. k ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) ) )
17 11 12 16 sylancl 
 |-  ( B e. On -> ( E. h ( h : ( cf ` A ) --> B /\ A. r e. B E. t e. ( cf ` A ) r C_ ( h ` t ) ) -> E. c e. suc ( cf ` A ) E. k ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) ) )
18 12 onsuci 
 |-  suc ( cf ` A ) e. On
19 18 oneli 
 |-  ( c e. suc ( cf ` A ) -> c e. On )
20 cfflb 
 |-  ( ( B e. On /\ c e. On ) -> ( E. k ( k : c --> B /\ A. r e. B E. s e. c r C_ ( k ` s ) ) -> ( cf ` B ) C_ c ) )
21 19 20 sylan2 
 |-  ( ( B e. On /\ c e. suc ( cf ` A ) ) -> ( E. k ( k : c --> B /\ A. r e. B E. s e. c r C_ ( k ` s ) ) -> ( cf ` B ) C_ c ) )
22 3simpb 
 |-  ( ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) -> ( k : c --> B /\ A. r e. B E. s e. c r C_ ( k ` s ) ) )
23 22 eximi 
 |-  ( E. k ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) -> E. k ( k : c --> B /\ A. r e. B E. s e. c r C_ ( k ` s ) ) )
24 21 23 impel 
 |-  ( ( ( B e. On /\ c e. suc ( cf ` A ) ) /\ E. k ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) ) -> ( cf ` B ) C_ c )
25 onsssuc 
 |-  ( ( c e. On /\ ( cf ` A ) e. On ) -> ( c C_ ( cf ` A ) <-> c e. suc ( cf ` A ) ) )
26 19 12 25 sylancl 
 |-  ( c e. suc ( cf ` A ) -> ( c C_ ( cf ` A ) <-> c e. suc ( cf ` A ) ) )
27 26 ibir 
 |-  ( c e. suc ( cf ` A ) -> c C_ ( cf ` A ) )
28 27 ad2antlr 
 |-  ( ( ( B e. On /\ c e. suc ( cf ` A ) ) /\ E. k ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) ) -> c C_ ( cf ` A ) )
29 24 28 sstrd 
 |-  ( ( ( B e. On /\ c e. suc ( cf ` A ) ) /\ E. k ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) ) -> ( cf ` B ) C_ ( cf ` A ) )
30 29 rexlimdva2 
 |-  ( B e. On -> ( E. c e. suc ( cf ` A ) E. k ( k : c --> B /\ Smo k /\ A. r e. B E. s e. c r C_ ( k ` s ) ) -> ( cf ` B ) C_ ( cf ` A ) ) )
31 17 30 syld 
 |-  ( B e. On -> ( E. h ( h : ( cf ` A ) --> B /\ A. r e. B E. t e. ( cf ` A ) r C_ ( h ` t ) ) -> ( cf ` B ) C_ ( cf ` A ) ) )
32 10 31 sylan9 
 |-  ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( cf ` B ) C_ ( cf ` A ) ) )
33 32 imp 
 |-  ( ( ( A e. On /\ B e. On ) /\ E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( cf ` B ) C_ ( cf ` A ) )
34 2 33 eqssd 
 |-  ( ( ( A e. On /\ B e. On ) /\ E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( cf ` A ) = ( cf ` B ) )
35 34 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( E. f ( f : B --> A /\ Smo f /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> ( cf ` A ) = ( cf ` B ) ) )