Metamath Proof Explorer

Theorem cflim3

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

Ref Expression
Hypothesis cflim3.1 
|- A e. _V
Assertion cflim3 
|- ( Lim A -> ( cf ` A ) = |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) )

Proof

Step Hyp Ref Expression
1 cflim3.1 
 |-  A e. _V
2 limord 
 |-  ( Lim A -> Ord A )
3 1 elon 
 |-  ( A e. On <-> Ord A )
4 2 3 sylibr 
 |-  ( Lim A -> A e. On )
5 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 ) ) } )
6 4 5 syl 
 |-  ( Lim A -> ( cf ` A ) = |^| { y | E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) } )
7 fvex 
 |-  ( card ` x ) e. _V
8 7 dfiin2 
 |-  |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) = |^| { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) }
9 df-rex 
 |-  ( E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) <-> E. x ( x e. { x e. ~P A | U. x = A } /\ y = ( card ` x ) ) )
10 ancom 
 |-  ( ( x e. { x e. ~P A | U. x = A } /\ y = ( card ` x ) ) <-> ( y = ( card ` x ) /\ x e. { x e. ~P A | U. x = A } ) )
11 rabid 
 |-  ( x e. { x e. ~P A | U. x = A } <-> ( x e. ~P A /\ U. x = A ) )
12 velpw 
 |-  ( x e. ~P A <-> x C_ A )
13 12 anbi1i 
 |-  ( ( x e. ~P A /\ U. x = A ) <-> ( x C_ A /\ U. x = A ) )
14 coflim 
 |-  ( ( Lim A /\ x C_ A ) -> ( U. x = A <-> A. z e. A E. w e. x z C_ w ) )
15 14 pm5.32da 
 |-  ( Lim A -> ( ( x C_ A /\ U. x = A ) <-> ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) )
16 13 15 bitrid 
 |-  ( Lim A -> ( ( x e. ~P A /\ U. x = A ) <-> ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) )
17 11 16 bitrid 
 |-  ( Lim A -> ( x e. { x e. ~P A | U. x = A } <-> ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) )
18 17 anbi2d 
 |-  ( Lim A -> ( ( y = ( card ` x ) /\ x e. { x e. ~P A | U. x = A } ) <-> ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) ) )
19 10 18 bitrid 
 |-  ( Lim A -> ( ( x e. { x e. ~P A | U. x = A } /\ y = ( card ` x ) ) <-> ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) ) )
20 19 exbidv 
 |-  ( Lim A -> ( E. x ( x e. { x e. ~P A | U. x = A } /\ y = ( card ` x ) ) <-> E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) ) )
21 9 20 bitrid 
 |-  ( Lim A -> ( E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) <-> E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) ) )
22 21 abbidv 
 |-  ( Lim A -> { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } = { y | E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) } )
23 22 inteqd 
 |-  ( Lim A -> |^| { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } = |^| { y | E. x ( y = ( card ` x ) /\ ( x C_ A /\ A. z e. A E. w e. x z C_ w ) ) } )
24 8 23 eqtr2id 
 |-  ( Lim A -> |^| { 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 | U. x = A } ( card ` x ) )
25 6 24 eqtrd 
 |-  ( Lim A -> ( cf ` A ) = |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) )