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) Avoid ax-11 . (Revised by BTernaryTau, 25-Jul-2025)

	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		fveq2	|- ( y = v -> ( card ` y ) = ( card ` v ) )
19	18	eqeq2d	|- ( y = v -> ( x = ( card ` y ) <-> x = ( card ` v ) ) )
20		sseq1	|- ( y = v -> ( y C_ A <-> v C_ A ) )
21		rexeq	|- ( y = v -> ( E. w e. y z C_ w <-> E. w e. v z C_ w ) )
22	21	ralbidv	|- ( y = v -> ( A. z e. A E. w e. y z C_ w <-> A. z e. A E. w e. v z C_ w ) )
23	20 22	anbi12d	|- ( y = v -> ( ( y C_ A /\ A. z e. A E. w e. y z C_ w ) <-> ( v C_ A /\ A. z e. A E. w e. v z C_ w ) ) )
24	19 23	anbi12d	|- ( y = v -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( x = ( card ` v ) /\ ( v C_ A /\ A. z e. A E. w e. v z C_ w ) ) ) )
25	24	excomimw	|- ( 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 ) ) )
26	17 25	sylbir	|- ( 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 ) ) )
27	12 26	syl	|- ( A e. V -> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )