Theorem xp2dju

Description: Two times a cardinal number. Exercise 4.56(g) of Mendelson p. 258. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	xp2dju	⊢ ( 2o × 𝐴 ) = ( 𝐴 ⊔ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		xpundir	⊢ ( ( { ∅ } ∪ { 1o } ) × 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) )
2		df2o3	⊢ 2o = { ∅ , 1o }
3		df-pr	⊢ { ∅ , 1o } = ( { ∅ } ∪ { 1o } )
4	2 3	eqtri	⊢ 2o = ( { ∅ } ∪ { 1o } )
5	4	xpeq1i	⊢ ( 2o × 𝐴 ) = ( ( { ∅ } ∪ { 1o } ) × 𝐴 )
6		df-dju	⊢ ( 𝐴 ⊔ 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) )
7	1 5 6	3eqtr4i	⊢ ( 2o × 𝐴 ) = ( 𝐴 ⊔ 𝐴 )