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

Metamath Proof Explorer

Theorem cflemOLD

Description: Obsolete version of cflem as of 25-Jul-2025. (Contributed by NM, 24-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cflemOLD 
|- ( 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 ) ) )