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