Theorem cflem 9068

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

Assertion

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

Distinct variable group:   x, y, z, w, A

Allowed substitution hints:   V( x, y, z, w)

Proof of Theorem cflem

Step	Hyp	Ref	Expression
1		ssid 3624	. . 3 |- A C_ A
2		ssid 3624	. . . . 5 |- z C_ z
3		sseq2 3627	. . . . . 6 |- ( w = z -> ( z C_ w <-> z C_ z ) )
4	3	rspcev 3309	. . . . 5 |- ( ( z e. A /\ z C_ z ) -> E. w e. A z C_ w )
5	2, 4	mpan2 707	. . . 4 |- ( z e. A -> E. w e. A z C_ w )
6	5	rgen 2922	. . 3 |- A. z e. A E. w e. A z C_ w
7		sseq1 3626	. . . . 5 |- ( y = A -> ( y C_ A <-> A C_ A ) )
8		rexeq 3139	. . . . . 6 |- ( y = A -> ( E. w e. y z C_ w <-> E. w e. A z C_ w ) )
9	8	ralbidv 2986	. . . . 5 |- ( 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 747	. . . 4 |- ( 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 3294	. . 3 |- ( 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 714	. 2 |- ( A e. V -> E. y ( y C_ A /\ A. z e. A E. w e. y z C_ w ) )
13		fvex 6201	. . . . . 6 |- ( card ` y ) e. _V
14	13	isseti 3209	. . . . 5 |- E. x x = ( card ` y )
15		19.41v 1914	. . . . 5 |- ( 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 953	. . . 4 |- ( 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 1774	. . 3 |- ( 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 2042	. . 3 |- ( 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 266	. 2 |- ( 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 208	1 |- ( A e. V -> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   C_ wss 3574   ` cfv 5888   cardccrd 8761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-fv 5896

This theorem is referenced by:  cfval  9069  cff  9070  cff1  9080