Metamath Proof Explorer

Theorem ficardun

Description: The cardinality of the union of disjoint, finite sets is the ordinal sum of their cardinalities. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Mario Carneiro, 28-Apr-2015) Avoid ax-rep . (Revised by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardun 
|- ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( A u. B ) ) = ( ( card ` A ) +o ( card ` B ) ) )

Proof

Step Hyp Ref Expression
1 ficardadju 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )
2 1 3adant3 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )
3 2 ensymd 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) )
4 endjudisj 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( A |_| B ) ~~ ( A u. B ) )
5 entr 
 |-  ( ( ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) /\ ( A |_| B ) ~~ ( A u. B ) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A u. B ) )
6 3 4 5 syl2anc 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A u. B ) )
7 carden2b 
 |-  ( ( ( card ` A ) +o ( card ` B ) ) ~~ ( A u. B ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( card ` ( A u. B ) ) )
8 6 7 syl 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( card ` ( A u. B ) ) )
9 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
10 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
11 nnacl 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( card ` A ) +o ( card ` B ) ) e. _om )
12 cardnn 
 |-  ( ( ( card ` A ) +o ( card ` B ) ) e. _om -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
13 11 12 syl 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
14 9 10 13 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
15 14 3adant3 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
16 8 15 eqtr3d 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( A u. B ) ) = ( ( card ` A ) +o ( card ` B ) ) )