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	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) ~~ ( A |_| B ) )

Proof

Step	Hyp	Ref	Expression
1		enrefg	|- ( A e. On -> A ~~ A )
2	1	adantr	|- ( ( A e. On /\ B e. On ) -> A ~~ A )
3		simpr	|- ( ( A e. On /\ B e. On ) -> B e. On )
4		eqid	|- ( x e. B |-> ( A +o x ) ) = ( x e. B |-> ( A +o x ) )
5	4	oacomf1olem	|- ( ( B e. On /\ A e. On ) -> ( ( x e. B |-> ( A +o x ) ) : B -1-1-onto-> ran ( x e. B |-> ( A +o x ) ) /\ ( ran ( x e. B |-> ( A +o x ) ) i^i A ) = (/) ) )
6	5	ancoms	|- ( ( A e. On /\ B e. On ) -> ( ( x e. B |-> ( A +o x ) ) : B -1-1-onto-> ran ( x e. B |-> ( A +o x ) ) /\ ( ran ( x e. B |-> ( A +o x ) ) i^i A ) = (/) ) )
7	6	simpld	|- ( ( A e. On /\ B e. On ) -> ( x e. B |-> ( A +o x ) ) : B -1-1-onto-> ran ( x e. B |-> ( A +o x ) ) )
8		f1oeng	|- ( ( B e. On /\ ( x e. B |-> ( A +o x ) ) : B -1-1-onto-> ran ( x e. B |-> ( A +o x ) ) ) -> B ~~ ran ( x e. B |-> ( A +o x ) ) )
9	3 7 8	syl2anc	|- ( ( A e. On /\ B e. On ) -> B ~~ ran ( x e. B |-> ( A +o x ) ) )
10		incom	|- ( A i^i ran ( x e. B |-> ( A +o x ) ) ) = ( ran ( x e. B |-> ( A +o x ) ) i^i A )
11	6	simprd	|- ( ( A e. On /\ B e. On ) -> ( ran ( x e. B |-> ( A +o x ) ) i^i A ) = (/) )
12	10 11	eqtrid	|- ( ( A e. On /\ B e. On ) -> ( A i^i ran ( x e. B |-> ( A +o x ) ) ) = (/) )
13		djuenun	|- ( ( A ~~ A /\ B ~~ ran ( x e. B |-> ( A +o x ) ) /\ ( A i^i ran ( x e. B |-> ( A +o x ) ) ) = (/) ) -> ( A |_| B ) ~~ ( A u. ran ( x e. B |-> ( A +o x ) ) ) )
14	2 9 12 13	syl3anc	|- ( ( A e. On /\ B e. On ) -> ( A |_| B ) ~~ ( A u. ran ( x e. B |-> ( A +o x ) ) ) )
15		oarec	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( A u. ran ( x e. B |-> ( A +o x ) ) ) )
16	14 15	breqtrrd	|- ( ( A e. On /\ B e. On ) -> ( A |_| B ) ~~ ( A +o B ) )
17	16	ensymd	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) ~~ ( A |_| B ) )