# Metamath Proof Explorer

## Theorem dnnumch3

Description: Define an injection from a set into the ordinals using a choice 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 dnnumch3
`|- ( ph -> ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On )`

### 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 cnvimass
` |-  ( `' F " { x } ) C_ dom F`
5 1 tfr1
` |-  F Fn On`
6 fndm
` |-  ( F Fn On -> dom F = On )`
7 5 6 ax-mp
` |-  dom F = On`
8 4 7 sseqtri
` |-  ( `' F " { x } ) C_ On`
9 1 2 3 dnnumch2
` |-  ( ph -> A C_ ran F )`
10 9 sselda
` |-  ( ( ph /\ x e. A ) -> x e. ran F )`
11 inisegn0
` |-  ( x e. ran F <-> ( `' F " { x } ) =/= (/) )`
12 10 11 sylib
` |-  ( ( ph /\ x e. A ) -> ( `' F " { x } ) =/= (/) )`
13 oninton
` |-  ( ( ( `' F " { x } ) C_ On /\ ( `' F " { x } ) =/= (/) ) -> |^| ( `' F " { x } ) e. On )`
14 8 12 13 sylancr
` |-  ( ( ph /\ x e. A ) -> |^| ( `' F " { x } ) e. On )`
15 14 fmpttd
` |-  ( ph -> ( x e. A |-> |^| ( `' F " { x } ) ) : A --> On )`
16 1 2 3 dnnumch3lem
` |-  ( ( ph /\ v e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = |^| ( `' F " { v } ) )`
17 16 adantrr
` |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = |^| ( `' F " { v } ) )`
18 1 2 3 dnnumch3lem
` |-  ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )`
19 18 adantrl
` |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )`
20 17 19 eqeq12d
` |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) <-> |^| ( `' F " { v } ) = |^| ( `' F " { w } ) ) )`
21 fveq2
` |-  ( |^| ( `' F " { v } ) = |^| ( `' F " { w } ) -> ( F ` |^| ( `' F " { v } ) ) = ( F ` |^| ( `' F " { w } ) ) )`
22 21 adantl
` |-  ( ( ( ph /\ ( v e. A /\ w e. A ) ) /\ |^| ( `' F " { v } ) = |^| ( `' F " { w } ) ) -> ( F ` |^| ( `' F " { v } ) ) = ( F ` |^| ( `' F " { w } ) ) )`
23 cnvimass
` |-  ( `' F " { v } ) C_ dom F`
24 23 7 sseqtri
` |-  ( `' F " { v } ) C_ On`
25 9 sselda
` |-  ( ( ph /\ v e. A ) -> v e. ran F )`
26 inisegn0
` |-  ( v e. ran F <-> ( `' F " { v } ) =/= (/) )`
27 25 26 sylib
` |-  ( ( ph /\ v e. A ) -> ( `' F " { v } ) =/= (/) )`
28 onint
` |-  ( ( ( `' F " { v } ) C_ On /\ ( `' F " { v } ) =/= (/) ) -> |^| ( `' F " { v } ) e. ( `' F " { v } ) )`
29 24 27 28 sylancr
` |-  ( ( ph /\ v e. A ) -> |^| ( `' F " { v } ) e. ( `' F " { v } ) )`
30 fniniseg
` |-  ( F Fn On -> ( |^| ( `' F " { v } ) e. ( `' F " { v } ) <-> ( |^| ( `' F " { v } ) e. On /\ ( F ` |^| ( `' F " { v } ) ) = v ) ) )`
31 5 30 ax-mp
` |-  ( |^| ( `' F " { v } ) e. ( `' F " { v } ) <-> ( |^| ( `' F " { v } ) e. On /\ ( F ` |^| ( `' F " { v } ) ) = v ) )`
32 31 simprbi
` |-  ( |^| ( `' F " { v } ) e. ( `' F " { v } ) -> ( F ` |^| ( `' F " { v } ) ) = v )`
33 29 32 syl
` |-  ( ( ph /\ v e. A ) -> ( F ` |^| ( `' F " { v } ) ) = v )`
34 33 adantrr
` |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( F ` |^| ( `' F " { v } ) ) = v )`
35 34 adantr
` |-  ( ( ( ph /\ ( v e. A /\ w e. A ) ) /\ |^| ( `' F " { v } ) = |^| ( `' F " { w } ) ) -> ( F ` |^| ( `' F " { v } ) ) = v )`
36 cnvimass
` |-  ( `' F " { w } ) C_ dom F`
37 36 7 sseqtri
` |-  ( `' F " { w } ) C_ On`
38 9 sselda
` |-  ( ( ph /\ w e. A ) -> w e. ran F )`
39 inisegn0
` |-  ( w e. ran F <-> ( `' F " { w } ) =/= (/) )`
40 38 39 sylib
` |-  ( ( ph /\ w e. A ) -> ( `' F " { w } ) =/= (/) )`
41 onint
` |-  ( ( ( `' F " { w } ) C_ On /\ ( `' F " { w } ) =/= (/) ) -> |^| ( `' F " { w } ) e. ( `' F " { w } ) )`
42 37 40 41 sylancr
` |-  ( ( ph /\ w e. A ) -> |^| ( `' F " { w } ) e. ( `' F " { w } ) )`
43 fniniseg
` |-  ( F Fn On -> ( |^| ( `' F " { w } ) e. ( `' F " { w } ) <-> ( |^| ( `' F " { w } ) e. On /\ ( F ` |^| ( `' F " { w } ) ) = w ) ) )`
44 5 43 ax-mp
` |-  ( |^| ( `' F " { w } ) e. ( `' F " { w } ) <-> ( |^| ( `' F " { w } ) e. On /\ ( F ` |^| ( `' F " { w } ) ) = w ) )`
45 44 simprbi
` |-  ( |^| ( `' F " { w } ) e. ( `' F " { w } ) -> ( F ` |^| ( `' F " { w } ) ) = w )`
46 42 45 syl
` |-  ( ( ph /\ w e. A ) -> ( F ` |^| ( `' F " { w } ) ) = w )`
47 46 adantrl
` |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( F ` |^| ( `' F " { w } ) ) = w )`
48 47 adantr
` |-  ( ( ( ph /\ ( v e. A /\ w e. A ) ) /\ |^| ( `' F " { v } ) = |^| ( `' F " { w } ) ) -> ( F ` |^| ( `' F " { w } ) ) = w )`
49 22 35 48 3eqtr3d
` |-  ( ( ( ph /\ ( v e. A /\ w e. A ) ) /\ |^| ( `' F " { v } ) = |^| ( `' F " { w } ) ) -> v = w )`
50 49 ex
` |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( |^| ( `' F " { v } ) = |^| ( `' F " { w } ) -> v = w ) )`
51 20 50 sylbid
` |-  ( ( ph /\ ( v e. A /\ w e. A ) ) -> ( ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) -> v = w ) )`
52 51 ralrimivva
` |-  ( ph -> A. v e. A A. w e. A ( ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) -> v = w ) )`
53 dff13
` |-  ( ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On <-> ( ( x e. A |-> |^| ( `' F " { x } ) ) : A --> On /\ A. v e. A A. w e. A ( ( ( x e. A |-> |^| ( `' F " { x } ) ) ` v ) = ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) -> v = w ) ) )`
54 15 52 53 sylanbrc
` |-  ( ph -> ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On )`