This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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