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 | |
|
dnnumch.a | |
||
dnnumch.g | |
||
Assertion | dnnumch3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dnnumch.f | |
|
2 | dnnumch.a | |
|
3 | dnnumch.g | |
|
4 | cnvimass | |
|
5 | 1 | tfr1 | |
6 | 5 | fndmi | |
7 | 4 6 | sseqtri | |
8 | 1 2 3 | dnnumch2 | |
9 | 8 | sselda | |
10 | inisegn0 | |
|
11 | 9 10 | sylib | |
12 | oninton | |
|
13 | 7 11 12 | sylancr | |
14 | 13 | fmpttd | |
15 | 1 2 3 | dnnumch3lem | |
16 | 15 | adantrr | |
17 | 1 2 3 | dnnumch3lem | |
18 | 17 | adantrl | |
19 | 16 18 | eqeq12d | |
20 | fveq2 | |
|
21 | 20 | adantl | |
22 | cnvimass | |
|
23 | 22 6 | sseqtri | |
24 | 8 | sselda | |
25 | inisegn0 | |
|
26 | 24 25 | sylib | |
27 | onint | |
|
28 | 23 26 27 | sylancr | |
29 | fniniseg | |
|
30 | 5 29 | ax-mp | |
31 | 30 | simprbi | |
32 | 28 31 | syl | |
33 | 32 | adantrr | |
34 | 33 | adantr | |
35 | cnvimass | |
|
36 | 35 6 | sseqtri | |
37 | 8 | sselda | |
38 | inisegn0 | |
|
39 | 37 38 | sylib | |
40 | onint | |
|
41 | 36 39 40 | sylancr | |
42 | fniniseg | |
|
43 | 5 42 | ax-mp | |
44 | 43 | simprbi | |
45 | 41 44 | syl | |
46 | 45 | adantrl | |
47 | 46 | adantr | |
48 | 21 34 47 | 3eqtr3d | |
49 | 48 | ex | |
50 | 19 49 | sylbid | |
51 | 50 | ralrimivva | |
52 | dff13 | |
|
53 | 14 51 52 | sylanbrc | |