Theorem cfub

Description: An upper bound on cofinality. (Contributed by NM, 25-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

	Ref	Expression
Assertion	cfub	|- ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }

Proof

Step	Hyp	Ref	Expression
1		cfval	|- ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
2		dfss3	|- ( A C_ U. y <-> A. z e. A z e. U. y )
3		ssel	|- ( y C_ A -> ( w e. y -> w e. A ) )
4		onelon	|- ( ( A e. On /\ w e. A ) -> w e. On )
5	4	ex	|- ( A e. On -> ( w e. A -> w e. On ) )
6	3 5	sylan9r	|- ( ( A e. On /\ y C_ A ) -> ( w e. y -> w e. On ) )
7		onelss	|- ( w e. On -> ( z e. w -> z C_ w ) )
8	6 7	syl6	|- ( ( A e. On /\ y C_ A ) -> ( w e. y -> ( z e. w -> z C_ w ) ) )
9	8	imdistand	|- ( ( A e. On /\ y C_ A ) -> ( ( w e. y /\ z e. w ) -> ( w e. y /\ z C_ w ) ) )
10	9	ancomsd	|- ( ( A e. On /\ y C_ A ) -> ( ( z e. w /\ w e. y ) -> ( w e. y /\ z C_ w ) ) )
11	10	eximdv	|- ( ( A e. On /\ y C_ A ) -> ( E. w ( z e. w /\ w e. y ) -> E. w ( w e. y /\ z C_ w ) ) )
12		eluni	|- ( z e. U. y <-> E. w ( z e. w /\ w e. y ) )
13		df-rex	|- ( E. w e. y z C_ w <-> E. w ( w e. y /\ z C_ w ) )
14	11 12 13	3imtr4g	|- ( ( A e. On /\ y C_ A ) -> ( z e. U. y -> E. w e. y z C_ w ) )
15	14	ralimdv	|- ( ( A e. On /\ y C_ A ) -> ( A. z e. A z e. U. y -> A. z e. A E. w e. y z C_ w ) )
16	2 15	syl5bi	|- ( ( A e. On /\ y C_ A ) -> ( A C_ U. y -> A. z e. A E. w e. y z C_ w ) )
17	16	imdistanda	|- ( A e. On -> ( ( y C_ A /\ A C_ U. y ) -> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
18	17	anim2d	|- ( A e. On -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) -> ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
19	18	eximdv	|- ( A e. On -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
20	19	ss2abdv	|- ( A e. On -> { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
21		intss	|- ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
22	20 21	syl	|- ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
23	1 22	eqsstrd	|- ( A e. On -> ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
24		cff	|- cf : On --> On
25	24	fdmi	|- dom cf = On
26	25	eleq2i	|- ( A e. dom cf <-> A e. On )
27		ndmfv	|- ( -. A e. dom cf -> ( cf ` A ) = (/) )
28	26 27	sylnbir	|- ( -. A e. On -> ( cf ` A ) = (/) )
29		0ss	|- (/) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }
30	28 29	eqsstrdi	|- ( -. A e. On -> ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
31	23 30	pm2.61i	|- ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }