Metamath Proof Explorer

Theorem hashun

Description: The size of the union of disjoint finite sets is the sum of their sizes. (Contributed by Paul Chapman, 30-Nov-2012) (Revised by Mario Carneiro, 15-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 ficardun 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( card ` ( A u. B ) ) = ( ( card ` A ) +o ( card ` B ) ) )
2 1 fveq2d 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( A u. B ) ) ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` B ) ) ) )
3 unfi 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
4 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
5 4 hashgval 
 |-  ( ( A u. B ) e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( A u. B ) ) ) = ( # ` ( A u. B ) ) )
6 3 5 syl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( A u. B ) ) ) = ( # ` ( A u. B ) ) )
7 6 3adant3 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` ( A u. B ) ) ) = ( # ` ( A u. B ) ) )
8 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
9 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
10 4 hashgadd 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) ) )
11 8 9 10 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) ) )
12 4 hashgval 
 |-  ( A e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) = ( # ` A ) )
13 4 hashgval 
 |-  ( B e. Fin -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) = ( # ` B ) )
14 12 13 oveqan12d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` A ) ) + ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( card ` B ) ) ) = ( ( # ` A ) + ( # ` B ) ) )
15 11 14 eqtrd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( # ` A ) + ( # ` B ) ) )
16 15 3adant3 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( # ` A ) + ( # ` B ) ) )
17 2 7 16 3eqtr3d 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) + ( # ` B ) ) )