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 )