Metamath Proof Explorer

Theorem endisj

Description: Any two sets are equinumerous to two disjoint sets. Exercise 4.39 of Mendelson p. 255. (Contributed by NM, 16-Apr-2004)

Ref Expression
Hypotheses endisj.1 
|- A e. _V
endisj.2 
|- B e. _V
Assertion endisj 
|- E. x E. y ( ( x ~~ A /\ y ~~ B ) /\ ( x i^i y ) = (/) )

Proof

Step Hyp Ref Expression
1 endisj.1 
 |-  A e. _V
2 endisj.2 
 |-  B e. _V
3 0ex 
 |-  (/) e. _V
4 1 3 xpsnen 
 |-  ( A X. { (/) } ) ~~ A
5 1oex 
 |-  1o e. _V
6 2 5 xpsnen 
 |-  ( B X. { 1o } ) ~~ B
7 4 6 pm3.2i 
 |-  ( ( A X. { (/) } ) ~~ A /\ ( B X. { 1o } ) ~~ B )
8 xp01disj 
 |-  ( ( A X. { (/) } ) i^i ( B X. { 1o } ) ) = (/)
9 p0ex 
 |-  { (/) } e. _V
10 1 9 xpex 
 |-  ( A X. { (/) } ) e. _V
11 snex 
 |-  { 1o } e. _V
12 2 11 xpex 
 |-  ( B X. { 1o } ) e. _V
13 breq1 
 |-  ( x = ( A X. { (/) } ) -> ( x ~~ A <-> ( A X. { (/) } ) ~~ A ) )
14 breq1 
 |-  ( y = ( B X. { 1o } ) -> ( y ~~ B <-> ( B X. { 1o } ) ~~ B ) )
15 13 14 bi2anan9 
 |-  ( ( x = ( A X. { (/) } ) /\ y = ( B X. { 1o } ) ) -> ( ( x ~~ A /\ y ~~ B ) <-> ( ( A X. { (/) } ) ~~ A /\ ( B X. { 1o } ) ~~ B ) ) )
16 ineq12 
 |-  ( ( x = ( A X. { (/) } ) /\ y = ( B X. { 1o } ) ) -> ( x i^i y ) = ( ( A X. { (/) } ) i^i ( B X. { 1o } ) ) )
17 16 eqeq1d 
 |-  ( ( x = ( A X. { (/) } ) /\ y = ( B X. { 1o } ) ) -> ( ( x i^i y ) = (/) <-> ( ( A X. { (/) } ) i^i ( B X. { 1o } ) ) = (/) ) )
18 15 17 anbi12d 
 |-  ( ( x = ( A X. { (/) } ) /\ y = ( B X. { 1o } ) ) -> ( ( ( x ~~ A /\ y ~~ B ) /\ ( x i^i y ) = (/) ) <-> ( ( ( A X. { (/) } ) ~~ A /\ ( B X. { 1o } ) ~~ B ) /\ ( ( A X. { (/) } ) i^i ( B X. { 1o } ) ) = (/) ) ) )
19 10 12 18 spc2ev 
 |-  ( ( ( ( A X. { (/) } ) ~~ A /\ ( B X. { 1o } ) ~~ B ) /\ ( ( A X. { (/) } ) i^i ( B X. { 1o } ) ) = (/) ) -> E. x E. y ( ( x ~~ A /\ y ~~ B ) /\ ( x i^i y ) = (/) ) )
20 7 8 19 mp2an 
 |-  E. x E. y ( ( x ~~ A /\ y ~~ B ) /\ ( x i^i y ) = (/) )