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=recszVGAranz
dnnumch.a φAV
dnnumch.g φy𝒫AyGyy
Assertion dnnumch3 φxAF-1x:A1-1On

Proof

Step Hyp Ref Expression
1 dnnumch.f F=recszVGAranz
2 dnnumch.a φAV
3 dnnumch.g φy𝒫AyGyy
4 cnvimass F-1xdomF
5 1 tfr1 FFnOn
6 5 fndmi domF=On
7 4 6 sseqtri F-1xOn
8 1 2 3 dnnumch2 φAranF
9 8 sselda φxAxranF
10 inisegn0 xranFF-1x
11 9 10 sylib φxAF-1x
12 oninton F-1xOnF-1xF-1xOn
13 7 11 12 sylancr φxAF-1xOn
14 13 fmpttd φxAF-1x:AOn
15 1 2 3 dnnumch3lem φvAxAF-1xv=F-1v
16 15 adantrr φvAwAxAF-1xv=F-1v
17 1 2 3 dnnumch3lem φwAxAF-1xw=F-1w
18 17 adantrl φvAwAxAF-1xw=F-1w
19 16 18 eqeq12d φvAwAxAF-1xv=xAF-1xwF-1v=F-1w
20 fveq2 F-1v=F-1wFF-1v=FF-1w
21 20 adantl φvAwAF-1v=F-1wFF-1v=FF-1w
22 cnvimass F-1vdomF
23 22 6 sseqtri F-1vOn
24 8 sselda φvAvranF
25 inisegn0 vranFF-1v
26 24 25 sylib φvAF-1v
27 onint F-1vOnF-1vF-1vF-1v
28 23 26 27 sylancr φvAF-1vF-1v
29 fniniseg FFnOnF-1vF-1vF-1vOnFF-1v=v
30 5 29 ax-mp F-1vF-1vF-1vOnFF-1v=v
31 30 simprbi F-1vF-1vFF-1v=v
32 28 31 syl φvAFF-1v=v
33 32 adantrr φvAwAFF-1v=v
34 33 adantr φvAwAF-1v=F-1wFF-1v=v
35 cnvimass F-1wdomF
36 35 6 sseqtri F-1wOn
37 8 sselda φwAwranF
38 inisegn0 wranFF-1w
39 37 38 sylib φwAF-1w
40 onint F-1wOnF-1wF-1wF-1w
41 36 39 40 sylancr φwAF-1wF-1w
42 fniniseg FFnOnF-1wF-1wF-1wOnFF-1w=w
43 5 42 ax-mp F-1wF-1wF-1wOnFF-1w=w
44 43 simprbi F-1wF-1wFF-1w=w
45 41 44 syl φwAFF-1w=w
46 45 adantrl φvAwAFF-1w=w
47 46 adantr φvAwAF-1v=F-1wFF-1w=w
48 21 34 47 3eqtr3d φvAwAF-1v=F-1wv=w
49 48 ex φvAwAF-1v=F-1wv=w
50 19 49 sylbid φvAwAxAF-1xv=xAF-1xwv=w
51 50 ralrimivva φvAwAxAF-1xv=xAF-1xwv=w
52 dff13 xAF-1x:A1-1OnxAF-1x:AOnvAwAxAF-1xv=xAF-1xwv=w
53 14 51 52 sylanbrc φxAF-1x:A1-1On