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 + 1 0 ↾ ω ⁡ card ⁡ A ∪ B = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A + 𝑜 card ⁡ B
3 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
4 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
5 4 hashgval ⊢ A ∪ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A ∪ B = A ∪ B
6 3 5 syl ⊢ A ∈ Fin ∧ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A ∪ B = A ∪ B
7 6 3adant3 ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ 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 + 1 0 ↾ ω ⁡ card ⁡ A + 𝑜 card ⁡ B = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A + rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ B
11 8 9 10 syl2an ⊢ A ∈ Fin ∧ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A + 𝑜 card ⁡ B = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A + rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ B
12 4 hashgval ⊢ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A = A
13 4 hashgval ⊢ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ B = B
14 12 13 oveqan12d ⊢ A ∈ Fin ∧ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A + rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ B = A + B
15 11 14 eqtrd ⊢ A ∈ Fin ∧ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A + 𝑜 card ⁡ B = A + B
16 15 3adant3 ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A + 𝑜 card ⁡ B = A + B
17 2 7 16 3eqtr3d ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → A ∪ B = A + B