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

Metamath Proof Explorer

Theorem hashuni

Description: The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Hypotheses hashuni.1 ⊢ φ → A ∈ Fin
hashuni.2 ⊢ φ → A ⊆ Fin
hashuni.3 ⊢ φ → Disj x ∈ A x
Assertion hashuni ⊢ φ → ⋃ A = ∑ x ∈ A x

Proof

Step Hyp Ref Expression
1 hashuni.1 ⊢ φ → A ∈ Fin
2 hashuni.2 ⊢ φ → A ⊆ Fin
3 hashuni.3 ⊢ φ → Disj x ∈ A x
4 uniiun ⊢ ⋃ A = ⋃ x ∈ A x
5 4 fveq2i ⊢ ⋃ A = ⋃ x ∈ A x
6 2 sselda ⊢ φ ∧ x ∈ A → x ∈ Fin
7 1 6 3 hashiun ⊢ φ → ⋃ x ∈ A x = ∑ x ∈ A x
8 5 7 eqtrid ⊢ φ → ⋃ A = ∑ x ∈ A x