Metamath Proof Explorer


Theorem onadju

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 AOnBOnA+𝑜BA⊔︀B

Proof

Step Hyp Ref Expression
1 enrefg AOnAA
2 1 adantr AOnBOnAA
3 simpr AOnBOnBOn
4 eqid xBA+𝑜x=xBA+𝑜x
5 4 oacomf1olem BOnAOnxBA+𝑜x:B1-1 ontoranxBA+𝑜xranxBA+𝑜xA=
6 5 ancoms AOnBOnxBA+𝑜x:B1-1 ontoranxBA+𝑜xranxBA+𝑜xA=
7 6 simpld AOnBOnxBA+𝑜x:B1-1 ontoranxBA+𝑜x
8 f1oeng BOnxBA+𝑜x:B1-1 ontoranxBA+𝑜xBranxBA+𝑜x
9 3 7 8 syl2anc AOnBOnBranxBA+𝑜x
10 incom AranxBA+𝑜x=ranxBA+𝑜xA
11 6 simprd AOnBOnranxBA+𝑜xA=
12 10 11 eqtrid AOnBOnAranxBA+𝑜x=
13 djuenun AABranxBA+𝑜xAranxBA+𝑜x=A⊔︀BAranxBA+𝑜x
14 2 9 12 13 syl3anc AOnBOnA⊔︀BAranxBA+𝑜x
15 oarec AOnBOnA+𝑜B=AranxBA+𝑜x
16 14 15 breqtrrd AOnBOnA⊔︀BA+𝑜B
17 16 ensymd AOnBOnA+𝑜BA⊔︀B