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

Metamath Proof Explorer

Theorem djuenun

Description: Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015) (Revised by Jim Kingdon, 19-Aug-2023)

		Ref	Expression
	Assertion	djuenun	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		djuen	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) )
2	1	3adant3	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) )
3		relen	⊢ Rel ≈
4	3	brrelex2i	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
5	3	brrelex2i	⊢ ( 𝐶 ≈ 𝐷 → 𝐷 ∈ V )
6		id	⊢ ( ( 𝐵 ∩ 𝐷 ) = ∅ → ( 𝐵 ∩ 𝐷 ) = ∅ )
7		endjudisj	⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐵 ⊔ 𝐷 ) ≈ ( 𝐵 ∪ 𝐷 ) )
8	4 5 6 7	syl3an	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐵 ⊔ 𝐷 ) ≈ ( 𝐵 ∪ 𝐷 ) )
9		entr	⊢ ( ( ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) ∧ ( 𝐵 ⊔ 𝐷 ) ≈ ( 𝐵 ∪ 𝐷 ) ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) )
10	2 8 9	syl2anc	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) )