Description: The cardinal and ordinal sums are always equinumerous. (Contributed by Mario Carneiro, 6-Feb-2013) (Revised by Jim Kingdon, 7-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | onadju | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enrefg | |
|
2 | 1 | adantr | |
3 | simpr | |
|
4 | eqid | |
|
5 | 4 | oacomf1olem | |
6 | 5 | ancoms | |
7 | 6 | simpld | |
8 | f1oeng | |
|
9 | 3 7 8 | syl2anc | |
10 | incom | |
|
11 | 6 | simprd | |
12 | 10 11 | eqtrid | |
13 | djuenun | |
|
14 | 2 9 12 13 | syl3anc | |
15 | oarec | |
|
16 | 14 15 | breqtrrd | |
17 | 16 | ensymd | |