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∈Fin∧B∈Fin∧A∩B=∅→A∪B=A+B

Proof

Step Hyp Ref Expression
1 ficardun ⊢A∈Fin∧B∈Fin∧A∩B=∅→card⁡A∪B=card⁡A+𝑜card⁡B
2 1 fveq2d ⊢A∈Fin∧B∈Fin∧A∩B=∅→rec⁡x∈V⟼x+10↾ω⁡card⁡A∪B=rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡B
3 unfi ⊢A∈Fin∧B∈Fin→A∪B∈Fin
4 eqid ⊢rec⁡x∈V⟼x+10↾ω=rec⁡x∈V⟼x+10↾ω
5 4 hashgval ⊢A∪B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A∪B=A∪B
6 3 5 syl ⊢A∈Fin∧B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A∪B=A∪B
7 6 3adant3 ⊢A∈Fin∧B∈Fin∧A∩B=∅→rec⁡x∈V⟼x+10↾ω⁡card⁡A∪B=A∪B
8 ficardom ⊢A∈Fin→card⁡A∈ω
9 ficardom ⊢B∈Fin→card⁡B∈ω
10 4 hashgadd ⊢card⁡A∈ω∧card⁡B∈ω→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡B=rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡B
11 8 9 10 syl2an ⊢A∈Fin∧B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡B=rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡B
12 4 hashgval ⊢A∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A=A
13 4 hashgval ⊢B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡B=B
14 12 13 oveqan12d ⊢A∈Fin∧B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+rec⁡x∈V⟼x+10↾ω⁡card⁡B=A+B
15 11 14 eqtrd ⊢A∈Fin∧B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡B=A+B
16 15 3adant3 ⊢A∈Fin∧B∈Fin∧A∩B=∅→rec⁡x∈V⟼x+10↾ω⁡card⁡A+𝑜card⁡B=A+B
17 2 7 16 3eqtr3d ⊢A∈Fin∧B∈Fin∧A∩B=∅→A∪B=A+B