This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( 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 ) )