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	|- ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( A |_| B ) ~~ ( A u. B ) )

Proof

Step	Hyp	Ref	Expression
1		df-dju	|- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
2		0ex	|- (/) e. _V
3		xpsnen2g	|- ( ( (/) e. _V /\ A e. V ) -> ( { (/) } X. A ) ~~ A )
4	2 3	mpan	|- ( A e. V -> ( { (/) } X. A ) ~~ A )
5		1on	|- 1o e. On
6		xpsnen2g	|- ( ( 1o e. On /\ B e. W ) -> ( { 1o } X. B ) ~~ B )
7	5 6	mpan	|- ( B e. W -> ( { 1o } X. B ) ~~ B )
8	4 7	anim12i	|- ( ( A e. V /\ B e. W ) -> ( ( { (/) } X. A ) ~~ A /\ ( { 1o } X. B ) ~~ B ) )
9		xp01disjl	|- ( ( { (/) } X. A ) i^i ( { 1o } X. B ) ) = (/)
10	9	jctl	|- ( ( A i^i B ) = (/) -> ( ( ( { (/) } X. A ) i^i ( { 1o } X. B ) ) = (/) /\ ( A i^i B ) = (/) ) )
11		unen	|- ( ( ( ( { (/) } X. A ) ~~ A /\ ( { 1o } X. B ) ~~ B ) /\ ( ( ( { (/) } X. A ) i^i ( { 1o } X. B ) ) = (/) /\ ( A i^i B ) = (/) ) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ~~ ( A u. B ) )
12	8 10 11	syl2an	|- ( ( ( A e. V /\ B e. W ) /\ ( A i^i B ) = (/) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ~~ ( A u. B ) )
13	12	3impa	|- ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ~~ ( A u. B ) )
14	1 13	eqbrtrid	|- ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( A |_| B ) ~~ ( A u. B ) )