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

Metamath Proof Explorer

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 ) )