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

Theorem xpfi 7848
Description: The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)
Assertion
Ref Expression
xpfi  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( A  X.  B
)  e.  Fin )

Proof of Theorem xpfi
Dummy variables  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpeq1 4868 . . . . 5  |-  ( x  =  (/)  ->  ( x  X.  B )  =  ( (/)  X.  B
) )
21eleq1d 2498 . . . 4  |-  ( x  =  (/)  ->  ( ( x  X.  B )  e.  Fin  <->  ( (/)  X.  B
)  e.  Fin )
)
32imbi2d 317 . . 3  |-  ( x  =  (/)  ->  ( ( B  e.  Fin  ->  ( x  X.  B )  e.  Fin )  <->  ( B  e.  Fin  ->  ( (/)  X.  B
)  e.  Fin )
) )
4 xpeq1 4868 . . . . 5  |-  ( x  =  ( y  \  { z } )  ->  ( x  X.  B )  =  ( ( y  \  {
z } )  X.  B ) )
54eleq1d 2498 . . . 4  |-  ( x  =  ( y  \  { z } )  ->  ( ( x  X.  B )  e. 
Fin 
<->  ( ( y  \  { z } )  X.  B )  e. 
Fin ) )
65imbi2d 317 . . 3  |-  ( x  =  ( y  \  { z } )  ->  ( ( B  e.  Fin  ->  (
x  X.  B )  e.  Fin )  <->  ( B  e.  Fin  ->  ( (
y  \  { z } )  X.  B
)  e.  Fin )
) )
7 xpeq1 4868 . . . . 5  |-  ( x  =  y  ->  (
x  X.  B )  =  ( y  X.  B ) )
87eleq1d 2498 . . . 4  |-  ( x  =  y  ->  (
( x  X.  B
)  e.  Fin  <->  ( y  X.  B )  e.  Fin ) )
98imbi2d 317 . . 3  |-  ( x  =  y  ->  (
( B  e.  Fin  ->  ( x  X.  B
)  e.  Fin )  <->  ( B  e.  Fin  ->  ( y  X.  B )  e.  Fin ) ) )
10 xpeq1 4868 . . . . 5  |-  ( x  =  A  ->  (
x  X.  B )  =  ( A  X.  B ) )
1110eleq1d 2498 . . . 4  |-  ( x  =  A  ->  (
( x  X.  B
)  e.  Fin  <->  ( A  X.  B )  e.  Fin ) )
1211imbi2d 317 . . 3  |-  ( x  =  A  ->  (
( B  e.  Fin  ->  ( x  X.  B
)  e.  Fin )  <->  ( B  e.  Fin  ->  ( A  X.  B )  e.  Fin ) ) )
13 0xp 4935 . . . . 5  |-  ( (/)  X.  B )  =  (/)
14 0fin 7805 . . . . 5  |-  (/)  e.  Fin
1513, 14eqeltri 2513 . . . 4  |-  ( (/)  X.  B )  e.  Fin
1615a1i 11 . . 3  |-  ( B  e.  Fin  ->  ( (/) 
X.  B )  e. 
Fin )
17 neq0 3778 . . . . . . 7  |-  ( -.  y  =  (/)  <->  E. w  w  e.  y )
18 sneq 4012 . . . . . . . . . . . . . . . 16  |-  ( z  =  w  ->  { z }  =  { w } )
1918difeq2d 3589 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  (
y  \  { z } )  =  ( y  \  { w } ) )
2019xpeq1d 4877 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  (
( y  \  {
z } )  X.  B )  =  ( ( y  \  {
w } )  X.  B ) )
2120eleq1d 2498 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
( ( y  \  { z } )  X.  B )  e. 
Fin 
<->  ( ( y  \  { w } )  X.  B )  e. 
Fin ) )
2221imbi2d 317 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( B  e.  Fin  ->  ( ( y  \  { z } )  X.  B )  e. 
Fin )  <->  ( B  e.  Fin  ->  ( (
y  \  { w } )  X.  B
)  e.  Fin )
) )
2322rspcv 3184 . . . . . . . . . . 11  |-  ( w  e.  y  ->  ( A. z  e.  y 
( B  e.  Fin  ->  ( ( y  \  { z } )  X.  B )  e. 
Fin )  ->  ( B  e.  Fin  ->  (
( y  \  {
w } )  X.  B )  e.  Fin ) ) )
2423adantl 467 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( A. z  e.  y  ( B  e.  Fin  ->  (
( y  \  {
z } )  X.  B )  e.  Fin )  ->  ( B  e. 
Fin  ->  ( ( y 
\  { w }
)  X.  B )  e.  Fin ) ) )
25 pm2.27 40 . . . . . . . . . . 11  |-  ( B  e.  Fin  ->  (
( B  e.  Fin  ->  ( ( y  \  { w } )  X.  B )  e. 
Fin )  ->  (
( y  \  {
w } )  X.  B )  e.  Fin ) )
2625ad2antlr 731 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( ( B  e.  Fin  ->  (
( y  \  {
w } )  X.  B )  e.  Fin )  ->  ( ( y 
\  { w }
)  X.  B )  e.  Fin ) )
27 snex 4663 . . . . . . . . . . . . . . 15  |-  { w }  e.  _V
28 xpexg 6607 . . . . . . . . . . . . . . 15  |-  ( ( { w }  e.  _V  /\  B  e.  Fin )  ->  ( { w }  X.  B )  e. 
_V )
2927, 28mpan 674 . . . . . . . . . . . . . 14  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  e.  _V )
30 id 23 . . . . . . . . . . . . . 14  |-  ( B  e.  Fin  ->  B  e.  Fin )
31 vex 3090 . . . . . . . . . . . . . . 15  |-  w  e. 
_V
32 2ndconst 6896 . . . . . . . . . . . . . . 15  |-  ( w  e.  _V  ->  ( 2nd  |`  ( { w }  X.  B ) ) : ( { w }  X.  B ) -1-1-onto-> B )
3331, 32mp1i 13 . . . . . . . . . . . . . 14  |-  ( B  e.  Fin  ->  ( 2nd  |`  ( { w }  X.  B ) ) : ( { w }  X.  B ) -1-1-onto-> B )
34 f1oen2g 7593 . . . . . . . . . . . . . 14  |-  ( ( ( { w }  X.  B )  e.  _V  /\  B  e.  Fin  /\  ( 2nd  |`  ( {
w }  X.  B
) ) : ( { w }  X.  B ) -1-1-onto-> B )  ->  ( { w }  X.  B )  ~~  B
)
3529, 30, 33, 34syl3anc 1264 . . . . . . . . . . . . 13  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  ~~  B
)
36 enfii 7795 . . . . . . . . . . . . 13  |-  ( ( B  e.  Fin  /\  ( { w }  X.  B )  ~~  B
)  ->  ( {
w }  X.  B
)  e.  Fin )
3735, 36mpdan 672 . . . . . . . . . . . 12  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  e.  Fin )
3837ad2antlr 731 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( {
w }  X.  B
)  e.  Fin )
39 unfi 7844 . . . . . . . . . . . 12  |-  ( ( ( ( y  \  { w } )  X.  B )  e. 
Fin  /\  ( {
w }  X.  B
)  e.  Fin )  ->  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin )
40 xpundir 4908 . . . . . . . . . . . . . . . 16  |-  ( ( ( y  \  {
w } )  u. 
{ w } )  X.  B )  =  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )
41 difsnid 4149 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  y  ->  (
( y  \  {
w } )  u. 
{ w } )  =  y )
4241xpeq1d 4877 . . . . . . . . . . . . . . . 16  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  u.  { w }
)  X.  B )  =  ( y  X.  B ) )
4340, 42syl5eqr 2484 . . . . . . . . . . . . . . 15  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  X.  B )  u.  ( { w }  X.  B ) )  =  ( y  X.  B
) )
4443eleq1d 2498 . . . . . . . . . . . . . 14  |-  ( w  e.  y  ->  (
( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin  <->  ( y  X.  B )  e.  Fin ) )
4544biimpd 210 . . . . . . . . . . . . 13  |-  ( w  e.  y  ->  (
( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin  ->  (
y  X.  B )  e.  Fin ) )
4645adantl 467 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( (
( ( y  \  { w } )  X.  B )  u.  ( { w }  X.  B ) )  e. 
Fin  ->  ( y  X.  B )  e.  Fin ) )
4739, 46syl5 33 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( (
( ( y  \  { w } )  X.  B )  e. 
Fin  /\  ( {
w }  X.  B
)  e.  Fin )  ->  ( y  X.  B
)  e.  Fin )
)
4838, 47mpan2d 678 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( (
( y  \  {
w } )  X.  B )  e.  Fin  ->  ( y  X.  B
)  e.  Fin )
)
4924, 26, 483syld 57 . . . . . . . . 9  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( A. z  e.  y  ( B  e.  Fin  ->  (
( y  \  {
z } )  X.  B )  e.  Fin )  ->  ( y  X.  B )  e.  Fin ) )
5049ex 435 . . . . . . . 8  |-  ( ( y  e.  Fin  /\  B  e.  Fin )  ->  ( w  e.  y  ->  ( A. z  e.  y  ( B  e.  Fin  ->  ( (
y  \  { z } )  X.  B
)  e.  Fin )  ->  ( y  X.  B
)  e.  Fin )
) )
5150exlimdv 1771 . . . . . . 7  |-  ( ( y  e.  Fin  /\  B  e.  Fin )  ->  ( E. w  w  e.  y  ->  ( A. z  e.  y 
( B  e.  Fin  ->  ( ( y  \  { z } )  X.  B )  e. 
Fin )  ->  (
y  X.  B )  e.  Fin ) ) )
5217, 51syl5bi 220 . . . . . 6  |-  ( ( y  e.  Fin  /\  B  e.  Fin )  ->  ( -.  y  =  (/)  ->  ( A. z  e.  y  ( B  e.  Fin  ->  ( (
y  \  { z } )  X.  B
)  e.  Fin )  ->  ( y  X.  B
)  e.  Fin )
) )
53 xpeq1 4868 . . . . . . . 8  |-  ( y  =  (/)  ->  ( y  X.  B )  =  ( (/)  X.  B
) )
5453, 15syl6eqel 2525 . . . . . . 7  |-  ( y  =  (/)  ->  ( y  X.  B )  e. 
Fin )
5554a1d 26 . . . . . 6  |-  ( y  =  (/)  ->  ( A. z  e.  y  ( B  e.  Fin  ->  (
( y  \  {
z } )  X.  B )  e.  Fin )  ->  ( y  X.  B )  e.  Fin ) )
5652, 55pm2.61d2 163 . . . . 5  |-  ( ( y  e.  Fin  /\  B  e.  Fin )  ->  ( A. z  e.  y  ( B  e. 
Fin  ->  ( ( y 
\  { z } )  X.  B )  e.  Fin )  -> 
( y  X.  B
)  e.  Fin )
)
5756ex 435 . . . 4  |-  ( y  e.  Fin  ->  ( B  e.  Fin  ->  ( A. z  e.  y 
( B  e.  Fin  ->  ( ( y  \  { z } )  X.  B )  e. 
Fin )  ->  (
y  X.  B )  e.  Fin ) ) )
5857com23 81 . . 3  |-  ( y  e.  Fin  ->  ( A. z  e.  y 
( B  e.  Fin  ->  ( ( y  \  { z } )  X.  B )  e. 
Fin )  ->  ( B  e.  Fin  ->  (
y  X.  B )  e.  Fin ) ) )
593, 6, 9, 12, 16, 58findcard 7816 . 2  |-  ( A  e.  Fin  ->  ( B  e.  Fin  ->  ( A  X.  B )  e. 
Fin ) )
6059imp 430 1  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( A  X.  B
)  e.  Fin )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    = wceq 1437   E.wex 1659    e. wcel 1870   A.wral 2782   _Vcvv 3087    \ cdif 3439    u. cun 3440   (/)c0 3767   {csn 4002   class class class wbr 4426    X. cxp 4852    |` cres 4856   -1-1-onto->wf1o 5600   2ndc2nd 6806    ~~ cen 7574   Fincfn 7577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-en 7578  df-fin 7581
This theorem is referenced by:  3xpfi  7849  mapfi  7876  fsuppxpfi  7906  infxpenlem  8443  ackbij1lem9  8656  ackbij1lem10  8657  hashxplem  12600  hashmap  12602  fsum2dlem  13809  fsumcom2  13813  ackbijnn  13864  fprod2dlem  14012  fprodcom2  14016  rexpen  14258  crt  14695  phimullem  14696  prmreclem3  14825  ablfaclem3  17655  gsumdixp  17772  gsumbagdiag  18535  psrass1lem  18536  evlslem2  18670  frlmbas3  19265  mamudm  19344  mamufacex  19345  mamures  19346  gsumcom3fi  19356  mamucl  19357  mamudi  19359  mamudir  19360  mamuvs1  19361  mamuvs2  19362  matsca2  19376  matbas2  19377  matplusg2  19383  matvsca2  19384  matplusgcell  19389  matsubgcell  19390  matvscacell  19392  matgsum  19393  mamumat1cl  19395  mattposcl  19409  mdetrsca  19559  mdetunilem9  19576  pmatcoe1fsupp  19656  tsmsxplem1  21098  tsmsxplem2  21099  tsmsxp  21100  i1fadd  22530  i1fmul  22531  itg1addlem4  22534  fsumdvdsmul  23987  fsumvma  24004  lgsquadlem1  24145  lgsquadlem2  24146  lgsquadlem3  24147  relfi  28052  sibfof  29001  erdszelem10  29711  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  cntotbnd  31832  pellex  35389  fourierdlem42  37580  etransclem44  37710  etransclem45  37711  etransclem47  37713
  Copyright terms: Public domain W3C validator