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 ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑥 𝑥 : 𝐴 –1-1-onto→ 𝐵 )
2 bren ⊢ ( 𝐶 ≈ 𝐷 ↔ ∃ 𝑦 𝑦 : 𝐶 –1-1-onto→ 𝐷 )
3 exdistrv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 : 𝐶 –1-1-onto→ 𝐷 ) ↔ ( ∃ 𝑥 𝑥 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ 𝑦 𝑦 : 𝐶 –1-1-onto→ 𝐷 ) )
4 vex ⊢ 𝑥 ∈ V
5 vex ⊢ 𝑦 ∈ V
6 4 5 unex ⊢ ( 𝑥 ∪ 𝑦 ) ∈ V
7 f1oun ⊢ ( ( ( 𝑥 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝑥 ∪ 𝑦 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) )
8 f1oen3g ⊢ ( ( ( 𝑥 ∪ 𝑦 ) ∈ V ∧ ( 𝑥 ∪ 𝑦 ) : ( 𝐴 ∪ 𝐶 ) –1-1-onto→ ( 𝐵 ∪ 𝐷 ) ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) )
9 6 7 8 sylancr ⊢ ( ( ( 𝑥 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) )
10 9 ex ⊢ ( ( 𝑥 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) ) )
11 10 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) ) )
12 3 11 sylbir ⊢ ( ( ∃ 𝑥 𝑥 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ 𝑦 𝑦 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) ) )
13 1 2 12 syl2anb ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) ) )
14 13 imp ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) ∧ ( ( 𝐴 ∩ 𝐶 ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) )