Metamath Proof Explorer

Theorem ficardadju

Description: The disjoint union of finite sets is equinumerous to the ordinal sum of the cardinalities of those sets. (Contributed by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardadju 
|- ( ( A e. Fin /\ B e. Fin ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )

Proof

Step Hyp Ref Expression
1 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
2 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
3 nnadju 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( card ` ( ( card ` A ) |_| ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
4 df-dju 
 |-  ( ( card ` A ) |_| ( card ` B ) ) = ( ( { (/) } X. ( card ` A ) ) u. ( { 1o } X. ( card ` B ) ) )
5 snfi 
 |-  { (/) } e. Fin
6 nnfi 
 |-  ( ( card ` A ) e. _om -> ( card ` A ) e. Fin )
7 xpfi 
 |-  ( ( { (/) } e. Fin /\ ( card ` A ) e. Fin ) -> ( { (/) } X. ( card ` A ) ) e. Fin )
8 5 6 7 sylancr 
 |-  ( ( card ` A ) e. _om -> ( { (/) } X. ( card ` A ) ) e. Fin )
9 snfi 
 |-  { 1o } e. Fin
10 nnfi 
 |-  ( ( card ` B ) e. _om -> ( card ` B ) e. Fin )
11 xpfi 
 |-  ( ( { 1o } e. Fin /\ ( card ` B ) e. Fin ) -> ( { 1o } X. ( card ` B ) ) e. Fin )
12 9 10 11 sylancr 
 |-  ( ( card ` B ) e. _om -> ( { 1o } X. ( card ` B ) ) e. Fin )
13 unfi 
 |-  ( ( ( { (/) } X. ( card ` A ) ) e. Fin /\ ( { 1o } X. ( card ` B ) ) e. Fin ) -> ( ( { (/) } X. ( card ` A ) ) u. ( { 1o } X. ( card ` B ) ) ) e. Fin )
14 8 12 13 syl2an 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( { (/) } X. ( card ` A ) ) u. ( { 1o } X. ( card ` B ) ) ) e. Fin )
15 4 14 eqeltrid 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( card ` A ) |_| ( card ` B ) ) e. Fin )
16 ficardid 
 |-  ( ( ( card ` A ) |_| ( card ` B ) ) e. Fin -> ( card ` ( ( card ` A ) |_| ( card ` B ) ) ) ~~ ( ( card ` A ) |_| ( card ` B ) ) )
17 15 16 syl 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( card ` ( ( card ` A ) |_| ( card ` B ) ) ) ~~ ( ( card ` A ) |_| ( card ` B ) ) )
18 3 17 eqbrtrrd 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( ( card ` A ) |_| ( card ` B ) ) )
19 1 2 18 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( ( card ` A ) |_| ( card ` B ) ) )
20 ficardid 
 |-  ( A e. Fin -> ( card ` A ) ~~ A )
21 ficardid 
 |-  ( B e. Fin -> ( card ` B ) ~~ B )
22 djuen 
 |-  ( ( ( card ` A ) ~~ A /\ ( card ` B ) ~~ B ) -> ( ( card ` A ) |_| ( card ` B ) ) ~~ ( A |_| B ) )
23 20 21 22 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) |_| ( card ` B ) ) ~~ ( A |_| B ) )
24 entr 
 |-  ( ( ( ( card ` A ) +o ( card ` B ) ) ~~ ( ( card ` A ) |_| ( card ` B ) ) /\ ( ( card ` A ) |_| ( card ` B ) ) ~~ ( A |_| B ) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) )
25 19 23 24 syl2anc 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) )
26 25 ensymd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )