MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unen Unicode version

Theorem unen 6945
Description: Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
unen  |-  ( ( ( A  ~~  B  /\  C  ~~  D )  /\  ( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) ) )  ->  ( A  u.  C )  ~~  ( B  u.  D )
)

Proof of Theorem unen
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 6873 . . 3  |-  ( A 
~~  B  <->  E. x  x : A -1-1-onto-> B )
2 bren 6873 . . 3  |-  ( C 
~~  D  <->  E. y 
y : C -1-1-onto-> D )
3 eeanv 1856 . . . 4  |-  ( E. x E. y ( x : A -1-1-onto-> B  /\  y : C -1-1-onto-> D )  <->  ( E. x  x : A -1-1-onto-> B  /\  E. y  y : C -1-1-onto-> D
) )
4 vex 2793 . . . . . . . 8  |-  x  e. 
_V
5 vex 2793 . . . . . . . 8  |-  y  e. 
_V
64, 5unex 4520 . . . . . . 7  |-  ( x  u.  y )  e. 
_V
7 f1oun 5494 . . . . . . 7  |-  ( ( ( x : A -1-1-onto-> B  /\  y : C -1-1-onto-> D )  /\  ( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) ) )  ->  ( x  u.  y ) : ( A  u.  C ) -1-1-onto-> ( B  u.  D ) )
8 f1oen3g 6879 . . . . . . 7  |-  ( ( ( x  u.  y
)  e.  _V  /\  ( x  u.  y
) : ( A  u.  C ) -1-1-onto-> ( B  u.  D ) )  ->  ( A  u.  C )  ~~  ( B  u.  D )
)
96, 7, 8sylancr 644 . . . . . 6  |-  ( ( ( x : A -1-1-onto-> B  /\  y : C -1-1-onto-> D )  /\  ( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) ) )  ->  ( A  u.  C )  ~~  ( B  u.  D )
)
109ex 423 . . . . 5  |-  ( ( x : A -1-1-onto-> B  /\  y : C -1-1-onto-> D )  ->  (
( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) )  ->  ( A  u.  C )  ~~  ( B  u.  D
) ) )
1110exlimivv 1669 . . . 4  |-  ( E. x E. y ( x : A -1-1-onto-> B  /\  y : C -1-1-onto-> D )  ->  (
( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) )  ->  ( A  u.  C )  ~~  ( B  u.  D
) ) )
123, 11sylbir 204 . . 3  |-  ( ( E. x  x : A -1-1-onto-> B  /\  E. y 
y : C -1-1-onto-> D )  ->  ( ( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) )  ->  ( A  u.  C )  ~~  ( B  u.  D
) ) )
131, 2, 12syl2anb 465 . 2  |-  ( ( A  ~~  B  /\  C  ~~  D )  -> 
( ( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) )  -> 
( A  u.  C
)  ~~  ( B  u.  D ) ) )
1413imp 418 1  |-  ( ( ( A  ~~  B  /\  C  ~~  D )  /\  ( ( A  i^i  C )  =  (/)  /\  ( B  i^i  D )  =  (/) ) )  ->  ( A  u.  C )  ~~  ( B  u.  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1530    = wceq 1625    e. wcel 1686   _Vcvv 2790    u. cun 3152    i^i cin 3153   (/)c0 3457   class class class wbr 4025   -1-1-onto->wf1o 5256    ~~ cen 6862
This theorem is referenced by:  difsnen  6946  undom  6952  limensuci  7039  infensuc  7041  phplem2  7043  pssnn  7083  dif1enOLD  7092  dif1en  7093  unfi  7126  infdifsn  7359  pm54.43  7635  dif1card  7640  cdaun  7800  cdaen  7801  ssfin4  7938  fin23lem26  7953  unsnen  8177  fzennn  11032  mreexexlem4d  13551
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-en 6866
  Copyright terms: Public domain W3C validator