Theorem djucomen

Description: Commutative law for cardinal addition. Exercise 4.56(c) of Mendelson p. 258. (Contributed by NM, 24-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	djucomen	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐵 ⊔ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		1oex	⊢ 1o ∈ V
2		xpsnen2g	⊢ ( ( 1o ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { 1o } × 𝐴 ) ≈ 𝐴 )
3	1 2	mpan	⊢ ( 𝐴 ∈ 𝑉 → ( { 1o } × 𝐴 ) ≈ 𝐴 )
4		0ex	⊢ ∅ ∈ V
5		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
6	4 5	mpan	⊢ ( 𝐵 ∈ 𝑊 → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
7		ensym	⊢ ( ( { 1o } × 𝐴 ) ≈ 𝐴 → 𝐴 ≈ ( { 1o } × 𝐴 ) )
8		ensym	⊢ ( ( { ∅ } × 𝐵 ) ≈ 𝐵 → 𝐵 ≈ ( { ∅ } × 𝐵 ) )
9		incom	⊢ ( ( { 1o } × 𝐴 ) ∩ ( { ∅ } × 𝐵 ) ) = ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐴 ) )
10		xp01disjl	⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐴 ) ) = ∅
11	9 10	eqtri	⊢ ( ( { 1o } × 𝐴 ) ∩ ( { ∅ } × 𝐵 ) ) = ∅
12		djuenun	⊢ ( ( 𝐴 ≈ ( { 1o } × 𝐴 ) ∧ 𝐵 ≈ ( { ∅ } × 𝐵 ) ∧ ( ( { 1o } × 𝐴 ) ∩ ( { ∅ } × 𝐵 ) ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
13	11 12	mp3an3	⊢ ( ( 𝐴 ≈ ( { 1o } × 𝐴 ) ∧ 𝐵 ≈ ( { ∅ } × 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
14	7 8 13	syl2an	⊢ ( ( ( { 1o } × 𝐴 ) ≈ 𝐴 ∧ ( { ∅ } × 𝐵 ) ≈ 𝐵 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
15	3 6 14	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) ) )
16		df-dju	⊢ ( 𝐵 ⊔ 𝐴 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐴 ) )
17	16	equncomi	⊢ ( 𝐵 ⊔ 𝐴 ) = ( ( { 1o } × 𝐴 ) ∪ ( { ∅ } × 𝐵 ) )
18	15 17	breqtrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐵 ⊔ 𝐴 ) )