Metamath Proof Explorer

Theorem ficardunOLD

Description: Obsolete version of ficardun as of 3-Jul-2024. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Mario Carneiro, 28-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ficardunOLD 
|- ( ( 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 finnum 
 |-  ( A e. Fin -> A e. dom card )
2 finnum 
 |-  ( B e. Fin -> B e. dom card )
3 cardadju 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )
5 4 3adant3 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )
6 5 ensymd 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) )
7 endjudisj 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( A |_| B ) ~~ ( A u. B ) )
8 entr 
 |-  ( ( ( ( card ` A ) +o ( card ` B ) ) ~~ ( A |_| B ) /\ ( A |_| B ) ~~ ( A u. B ) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A u. B ) )
9 6 7 8 syl2anc 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( ( card ` A ) +o ( card ` B ) ) ~~ ( A u. B ) )
10 carden2b 
 |-  ( ( ( card ` A ) +o ( card ` B ) ) ~~ ( A u. B ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( card ` ( A u. B ) ) )
11 9 10 syl 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( card ` ( A u. B ) ) )
12 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
13 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
14 nnacl 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( card ` A ) +o ( card ` B ) ) e. _om )
15 cardnn 
 |-  ( ( ( card ` A ) +o ( card ` B ) ) e. _om -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
16 14 15 syl 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
17 12 13 16 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
18 17 3adant3 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
19 11 18 eqtr3d 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( A u. B ) ) = ( ( card ` A ) +o ( card ` B ) ) )