# Metamath Proof Explorer

## 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 fndm
` |-  ( F Fn On -> dom F = On )`
12 10 11 ax-mp
` |-  dom F = On`
13 9 12 sseqtri
` |-  ( `' F " { w } ) C_ On`
14 1 2 3 dnnumch2
` |-  ( ph -> A C_ ran F )`
15 14 sselda
` |-  ( ( ph /\ w e. A ) -> w e. ran F )`
16 inisegn0
` |-  ( w e. ran F <-> ( `' F " { w } ) =/= (/) )`
17 15 16 sylib
` |-  ( ( ph /\ w e. A ) -> ( `' F " { w } ) =/= (/) )`
18 oninton
` |-  ( ( ( `' F " { w } ) C_ On /\ ( `' F " { w } ) =/= (/) ) -> |^| ( `' F " { w } ) e. On )`
19 13 17 18 sylancr
` |-  ( ( ph /\ w e. A ) -> |^| ( `' F " { w } ) e. On )`
20 4 7 8 19 fvmptd3
` |-  ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )`