This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ficardun ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
2 1 fveq2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) )
3 unfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
4 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
5 4 hashgval ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ) = ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) )
6 3 5 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ) = ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) )
7 6 3adant3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ) = ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) )
8 ficardom ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
9 ficardom ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω )
10 4 hashgadd ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) )
11 8 9 10 syl2an ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) )
12 4 hashgval ⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
13 4 hashgval ⊢ ( 𝐵 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) )
14 12 13 oveqan12d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
15 11 14 eqtrd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
16 15 3adant3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
17 2 7 16 3eqtr3d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )