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