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