Description: The set of hereditarily finite sets is countable. See ackbij2 for an explicit bijection that works without Infinity. See also r1omALT . (Contributed by Stefan O'Rear, 18-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | r1om | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omex | |
|
2 | limom | |
|
3 | r1lim | |
|
4 | 1 2 3 | mp2an | |
5 | r1fnon | |
|
6 | fnfun | |
|
7 | funiunfv | |
|
8 | 5 6 7 | mp2b | |
9 | 4 8 | eqtri | |
10 | iuneq1 | |
|
11 | sneq | |
|
12 | pweq | |
|
13 | 11 12 | xpeq12d | |
14 | 13 | cbviunv | |
15 | 10 14 | eqtrdi | |
16 | 15 | fveq2d | |
17 | 16 | cbvmptv | |
18 | dmeq | |
|
19 | 18 | pweqd | |
20 | imaeq1 | |
|
21 | 20 | fveq2d | |
22 | 19 21 | mpteq12dv | |
23 | imaeq2 | |
|
24 | 23 | fveq2d | |
25 | 24 | cbvmptv | |
26 | 22 25 | eqtrdi | |
27 | 26 | cbvmptv | |
28 | eqid | |
|
29 | 17 27 28 | ackbij2 | |
30 | fvex | |
|
31 | 9 30 | eqeltrri | |
32 | 31 | f1oen | |
33 | 29 32 | ax-mp | |
34 | 9 33 | eqbrtri | |