Theorem dnnumch3lem

Description: Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	dnnumch.f	|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
	dnnumch.a	|- ( ph -> A e. V )
	dnnumch.g	|- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
Assertion	dnnumch3lem	|- ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )

Proof

Step	Hyp	Ref	Expression
1		dnnumch.f	|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
2		dnnumch.a	|- ( ph -> A e. V )
3		dnnumch.g	|- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
4		eqid	|- ( x e. A |-> |^| ( `' F " { x } ) ) = ( x e. A |-> |^| ( `' F " { x } ) )
5		sneq	|- ( x = w -> { x } = { w } )
6	5	imaeq2d	|- ( x = w -> ( `' F " { x } ) = ( `' F " { w } ) )
7	6	inteqd	|- ( x = w -> |^| ( `' F " { x } ) = |^| ( `' F " { w } ) )
8		simpr	|- ( ( ph /\ w e. A ) -> w e. A )
9		cnvimass	|- ( `' F " { w } ) C_ dom F
10	1	tfr1	|- F Fn On
11	10	fndmi	|- dom F = On
12	9 11	sseqtri	|- ( `' F " { w } ) C_ On
13	1 2 3	dnnumch2	|- ( ph -> A C_ ran F )
14	13	sselda	|- ( ( ph /\ w e. A ) -> w e. ran F )
15		inisegn0	|- ( w e. ran F <-> ( `' F " { w } ) =/= (/) )
16	14 15	sylib	|- ( ( ph /\ w e. A ) -> ( `' F " { w } ) =/= (/) )
17		oninton	|- ( ( ( `' F " { w } ) C_ On /\ ( `' F " { w } ) =/= (/) ) -> |^| ( `' F " { w } ) e. On )
18	12 16 17	sylancr	|- ( ( ph /\ w e. A ) -> |^| ( `' F " { w } ) e. On )
19	4 7 8 18	fvmptd3	|- ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )