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