Theorem cflem

Description: A lemma used to simplify cofinality computations, showing the existence of the cardinal of an unbounded subset of a set A . (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	cflem	|- ( A e. V -> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- A C_ A
2		ssid	|- z C_ z
3		sseq2	|- ( w = z -> ( z C_ w <-> z C_ z ) )
4	3	rspcev	|- ( ( z e. A /\ z C_ z ) -> E. w e. A z C_ w )
5	2 4	mpan2	|- ( z e. A -> E. w e. A z C_ w )
6	5	rgen	|- A. z e. A E. w e. A z C_ w
7		sseq1	|- ( y = A -> ( y C_ A <-> A C_ A ) )
8		rexeq	|- ( y = A -> ( E. w e. y z C_ w <-> E. w e. A z C_ w ) )
9	8	ralbidv	|- ( y = A -> ( A. z e. A E. w e. y z C_ w <-> A. z e. A E. w e. A z C_ w ) )
10	7 9	anbi12d	|- ( y = A -> ( ( y C_ A /\ A. z e. A E. w e. y z C_ w ) <-> ( A C_ A /\ A. z e. A E. w e. A z C_ w ) ) )
11	10	spcegv	|- ( A e. V -> ( ( A C_ A /\ A. z e. A E. w e. A z C_ w ) -> E. y ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
12	1 6 11	mp2ani	|- ( A e. V -> E. y ( y C_ A /\ A. z e. A E. w e. y z C_ w ) )
13		fvex	|- ( card ` y ) e. _V
14	13	isseti	|- E. x x = ( card ` y )
15		19.41v	|- ( E. x ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( E. x x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
16	14 15	mpbiran	|- ( E. x ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) )
17	16	exbii	|- ( E. y E. x ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( y C_ A /\ A. z e. A E. w e. y z C_ w ) )
18		excom	|- ( E. y E. x ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
19	17 18	bitr3i	|- ( E. y ( y C_ A /\ A. z e. A E. w e. y z C_ w ) <-> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
20	12 19	sylib	|- ( A e. V -> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )