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