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

Metamath Proof Explorer

Theorem cff

Description: Cofinality is a function on the class of ordinal numbers to the class of cardinal numbers. (Contributed by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cff 
|- cf : On --> On

Proof

Step Hyp Ref Expression
1 df-cf 
 |-  cf = ( x e. On |-> |^| { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } )
2 cardon 
 |-  ( card ` z ) e. On
3 eleq1 
 |-  ( y = ( card ` z ) -> ( y e. On <-> ( card ` z ) e. On ) )
4 2 3 mpbiri 
 |-  ( y = ( card ` z ) -> y e. On )
5 4 adantr 
 |-  ( ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) -> y e. On )
6 5 exlimiv 
 |-  ( E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) -> y e. On )
7 6 abssi 
 |-  { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } C_ On
8 cflem 
 |-  ( x e. On -> E. y E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) )
9 abn0 
 |-  ( { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } =/= (/) <-> E. y E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) )
10 8 9 sylibr 
 |-  ( x e. On -> { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } =/= (/) )
11 oninton 
 |-  ( ( { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } C_ On /\ { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } =/= (/) ) -> |^| { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } e. On )
12 7 10 11 sylancr 
 |-  ( x e. On -> |^| { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. w e. x E. v e. z w C_ v ) ) } e. On )
13 1 12 fmpti 
 |-  cf : On --> On