Theorem endjudisj

Description: Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007)

	Ref	Expression
Assertion	endjudisj	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
2		0ex	⊢ ∅ ∈ V
3		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
4	2 3	mpan	⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
5		1on	⊢ 1o ∈ On
6		xpsnen2g	⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ 𝑊 ) → ( { 1o } × 𝐵 ) ≈ 𝐵 )
7	5 6	mpan	⊢ ( 𝐵 ∈ 𝑊 → ( { 1o } × 𝐵 ) ≈ 𝐵 )
8	4 7	anim12i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { ∅ } × 𝐴 ) ≈ 𝐴 ∧ ( { 1o } × 𝐵 ) ≈ 𝐵 ) )
9		xp01disjl	⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅
10	9	jctl	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅ ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
11		unen	⊢ ( ( ( ( { ∅ } × 𝐴 ) ≈ 𝐴 ∧ ( { 1o } × 𝐵 ) ≈ 𝐵 ) ∧ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅ ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 ∪ 𝐵 ) )
12	8 10 11	syl2an	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 ∪ 𝐵 ) )
13	12	3impa	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 ∪ 𝐵 ) )
14	1 13	eqbrtrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )