Theorem cfcof 8666

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.)

Assertion

Ref	Expression
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 ) ) )

Distinct variable groups:   w, f, z, A   B, f, w, z

Proof of Theorem cfcof

Dummy variables c g h k r s t x y v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cfcoflem 8664	. . . 4 |- ( ( 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 429	. . 3 |- ( ( ( 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 8650	. . . . . . 7 |- ( 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 5787	. . . . . . . . 9 |- ( g : ( cf ` A ) -1-1-> A -> g : ( cf ` A ) --> A )
5	4	anim1i 568	. . . . . . . 8 |- ( ( 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 1635	. . . . . . 7 |- ( 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 16	. . . . . 6 |- ( A e. On -> E. g ( g : ( cf ` A ) --> A /\ A. s e. A E. t e. ( cf ` A ) s C_ ( g ` t ) ) )
8		eqid 2467	. . . . . . 7 |- ( 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 8665	. . . . . 6 |- ( 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 30	. . . . 5 |- ( 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 4894	. . . . . . 7 |- ( B e. On -> Ord B )
12		cfon 8647	. . . . . . 7 |- ( cf ` A ) e. On
13		eqid 2467	. . . . . . . 8 |- { 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 2467	. . . . . . . 8 |- |^| { c e. ( cf ` A ) | r C_ ( h ` c ) } = |^| { c e. ( cf ` A ) | r C_ ( h ` c ) }
15		eqid 2467	. . . . . . . 8 |- 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 8661	. . . . . . 7 |- ( ( 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 662	. . . . . 6 |- ( 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		3simpb 994	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
19	18	eximi 1635	. . . . . . . . . . 11 |- ( 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 ) ) )
20	12	onsuci 6668	. . . . . . . . . . . . 13 |- suc ( cf ` A ) e. On
21	20	oneli 4991	. . . . . . . . . . . 12 |- ( c e. suc ( cf ` A ) -> c e. On )
22		cfflb 8651	. . . . . . . . . . . 12 |- ( ( 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 ) )
23	21, 22	sylan2 474	. . . . . . . . . . 11 |- ( ( 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 ) )
24	19, 23	syl5 32	. . . . . . . . . 10 |- ( ( 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	24	imp 429	. . . . . . . . 9 |- ( ( ( 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 )
26		onsssuc 4971	. . . . . . . . . . . 12 |- ( ( c e. On /\ ( cf ` A ) e. On ) -> ( c C_ ( cf ` A ) <-> c e. suc ( cf ` A ) ) )
27	21, 12, 26	sylancl 662	. . . . . . . . . . 11 |- ( c e. suc ( cf ` A ) -> ( c C_ ( cf ` A ) <-> c e. suc ( cf ` A ) ) )
28	27	ibir 242	. . . . . . . . . 10 |- ( c e. suc ( cf ` A ) -> c C_ ( cf ` A ) )
29	28	ad2antlr 726	. . . . . . . . 9 |- ( ( ( 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 ) )
30	25, 29	sstrd 3519	. . . . . . . 8 |- ( ( ( 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 ) )
31	30	exp31 604	. . . . . . 7 |- ( 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 ) ) ) )
32	31	rexlimdv 2957	. . . . . 6 |- ( 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 ) ) )
33	17, 32	syld 44	. . . . 5 |- ( 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 ) ) )
34	10, 33	sylan9 657	. . . 4 |- ( ( 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 ) ) )
35	34	imp 429	. . 3 |- ( ( ( 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 ) )
36	2, 35	eqssd 3526	. 2 |- ( ( ( 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 ) )
37	36	ex 434	1 |- ( ( 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 ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   E.wex 1596   e. wcel 1767   A.wral 2817   E.wrex 2818   {crab 2821   C_ wss 3481   |^|cint 4288   |-> cmpt 4511   _E cep 4795   Ord word 4883   Oncon0 4884   suc csuc 4886   -->wf 5590   -1-1->wf1 5591   ` cfv 5594   Smo wsmo 7028  OrdIsocoi 7946   cfccf 8330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6795  df-2nd 6796  df-smo 7029  df-recs 7054  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-oi 7947  df-card 8332  df-cf 8334  df-acn 8335

This theorem is referenced by:  alephsing  8668