Metamath Proof Explorer

Theorem cfval2

Description: Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion cfval2 
|- ( A e. On -> ( cf ` A ) = |^|_ x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } ( card ` x ) )

Proof

Step Hyp Ref Expression
1 cfval 
 |-  ( A e. On -> ( cf ` A ) = |^| { y | E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) } )
2 fvex 
 |-  ( card ` x ) e. _V
3 2 dfiin2 
 |-  |^|_ x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } ( card ` x ) = |^| { y | E. x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } y = ( card ` x ) }
4 df-rex 
 |-  ( E. x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } y = ( card ` x ) <-> E. x ( x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } /\ y = ( card ` x ) ) )
5 rabid 
 |-  ( x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } <-> ( x e. ~P A /\ A. z e. A E. w e. x z C_ w ) )
6 velpw 
 |-  ( x e. ~P A <-> x C_ A )
7 6 anbi1i 
 |-  ( ( x e. ~P A /\ A. z e. A E. w e. x z C_ w ) <-> ( x C_ A /\ A. z e. A E. w e. x z C_ w ) )
8 5 7 bitri 
 |-  ( x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } <-> ( x C_ A /\ A. z e. A E. w e. x z C_ w ) )
9 8 anbi2ci 
 |-  ( ( x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } /\ y = ( card ` x ) ) <-> ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) )
10 9 exbii 
 |-  ( E. x ( x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } /\ y = ( card ` x ) ) <-> E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) )
11 4 10 bitri 
 |-  ( E. x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } y = ( card ` x ) <-> E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) )
12 11 abbii 
 |-  { y | E. x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } y = ( card ` x ) } = { y | E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) }
13 12 inteqi 
 |-  |^| { y | E. x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } y = ( card ` x ) } = |^| { y | E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) }
14 3 13 eqtr2i 
 |-  |^| { y | E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) } = |^|_ x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } ( card ` x )
15 1 14 eqtrdi 
 |-  ( A e. On -> ( cf ` A ) = |^|_ x e. { x e. ~P A | A. z e. A E. w e. x z C_ w } ( card ` x ) )