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

Metamath Proof Explorer

Theorem cfsmo

Description: The map in cff1 can be assumed to be a strictly monotone ordinal function without loss of generality. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion cfsmo 
|- ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )

Proof

Step Hyp Ref Expression
1 dmeq 
 |-  ( x = z -> dom x = dom z )
2 1 fveq2d 
 |-  ( x = z -> ( h ` dom x ) = ( h ` dom z ) )
3 fveq2 
 |-  ( n = m -> ( x ` n ) = ( x ` m ) )
4 suceq 
 |-  ( ( x ` n ) = ( x ` m ) -> suc ( x ` n ) = suc ( x ` m ) )
5 3 4 syl 
 |-  ( n = m -> suc ( x ` n ) = suc ( x ` m ) )
6 5 cbviunv 
 |-  U_ n e. dom x suc ( x ` n ) = U_ m e. dom x suc ( x ` m )
7 fveq1 
 |-  ( x = z -> ( x ` m ) = ( z ` m ) )
8 suceq 
 |-  ( ( x ` m ) = ( z ` m ) -> suc ( x ` m ) = suc ( z ` m ) )
9 7 8 syl 
 |-  ( x = z -> suc ( x ` m ) = suc ( z ` m ) )
10 1 9 iuneq12d 
 |-  ( x = z -> U_ m e. dom x suc ( x ` m ) = U_ m e. dom z suc ( z ` m ) )
11 6 10 eqtrid 
 |-  ( x = z -> U_ n e. dom x suc ( x ` n ) = U_ m e. dom z suc ( z ` m ) )
12 2 11 uneq12d 
 |-  ( x = z -> ( ( h ` dom x ) u. U_ n e. dom x suc ( x ` n ) ) = ( ( h ` dom z ) u. U_ m e. dom z suc ( z ` m ) ) )
13 12 cbvmptv 
 |-  ( x e. _V |-> ( ( h ` dom x ) u. U_ n e. dom x suc ( x ` n ) ) ) = ( z e. _V |-> ( ( h ` dom z ) u. U_ m e. dom z suc ( z ` m ) ) )
14 eqid 
 |-  ( recs ( ( x e. _V |-> ( ( h ` dom x ) u. U_ n e. dom x suc ( x ` n ) ) ) ) |` ( cf ` A ) ) = ( recs ( ( x e. _V |-> ( ( h ` dom x ) u. U_ n e. dom x suc ( x ` n ) ) ) ) |` ( cf ` A ) )
15 13 14 cfsmolem 
 |-  ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )