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

Metamath Proof Explorer

Theorem unen

Description: Equinumerosity of union of disjoint sets. Theorem 4 of Suppes p. 92. (Contributed by NM, 11-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion unen ⊢ A ≈ B ∧ C ≈ D ∧ A ∩ C = ∅ ∧ B ∩ D = ∅ → A ∪ C ≈ B ∪ D

Proof

Step Hyp Ref Expression
1 bren ⊢ A ≈ B ↔ ∃ x x : A ⟶ 1-1 onto B
2 bren ⊢ C ≈ D ↔ ∃ y y : C ⟶ 1-1 onto D
3 exdistrv ⊢ ∃ x ∃ y x : A ⟶ 1-1 onto B ∧ y : C ⟶ 1-1 onto D ↔ ∃ x x : A ⟶ 1-1 onto B ∧ ∃ y y : C ⟶ 1-1 onto D
4 vex ⊢ x ∈ V
5 vex ⊢ y ∈ V
6 4 5 unex ⊢ x ∪ y ∈ V
7 f1oun ⊢ x : A ⟶ 1-1 onto B ∧ y : C ⟶ 1-1 onto D ∧ A ∩ C = ∅ ∧ B ∩ D = ∅ → x ∪ y : A ∪ C ⟶ 1-1 onto B ∪ D
8 f1oen3g ⊢ x ∪ y ∈ V ∧ x ∪ y : A ∪ C ⟶ 1-1 onto B ∪ D → A ∪ C ≈ B ∪ D
9 6 7 8 sylancr ⊢ x : A ⟶ 1-1 onto B ∧ y : C ⟶ 1-1 onto D ∧ A ∩ C = ∅ ∧ B ∩ D = ∅ → A ∪ C ≈ B ∪ D
10 9 ex ⊢ x : A ⟶ 1-1 onto B ∧ y : C ⟶ 1-1 onto D → A ∩ C = ∅ ∧ B ∩ D = ∅ → A ∪ C ≈ B ∪ D
11 10 exlimivv ⊢ ∃ x ∃ y x : A ⟶ 1-1 onto B ∧ y : C ⟶ 1-1 onto D → A ∩ C = ∅ ∧ B ∩ D = ∅ → A ∪ C ≈ B ∪ D
12 3 11 sylbir ⊢ ∃ x x : A ⟶ 1-1 onto B ∧ ∃ y y : C ⟶ 1-1 onto D → A ∩ C = ∅ ∧ B ∩ D = ∅ → A ∪ C ≈ B ∪ D
13 1 2 12 syl2anb ⊢ A ≈ B ∧ C ≈ D → A ∩ C = ∅ ∧ B ∩ D = ∅ → A ∪ C ≈ B ∪ D
14 13 imp ⊢ A ≈ B ∧ C ≈ D ∧ A ∩ C = ∅ ∧ B ∩ D = ∅ → A ∪ C ≈ B ∪ D