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

Theorem xpfi 7588
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 4859 . . . . 5  |-  ( x  =  (/)  ->  ( x  X.  B )  =  ( (/)  X.  B
) )
21eleq1d 2509 . . . 4  |-  ( x  =  (/)  ->  ( ( x  X.  B )  e.  Fin  <->  ( (/)  X.  B
)  e.  Fin )
)
32imbi2d 316 . . 3  |-  ( x  =  (/)  ->  ( ( B  e.  Fin  ->  ( x  X.  B )  e.  Fin )  <->  ( B  e.  Fin  ->  ( (/)  X.  B
)  e.  Fin )
) )
4 xpeq1 4859 . . . . 5  |-  ( x  =  ( y  \  { z } )  ->  ( x  X.  B )  =  ( ( y  \  {
z } )  X.  B ) )
54eleq1d 2509 . . . 4  |-  ( x  =  ( y  \  { z } )  ->  ( ( x  X.  B )  e. 
Fin 
<->  ( ( y  \  { z } )  X.  B )  e. 
Fin ) )
65imbi2d 316 . . 3  |-  ( x  =  ( y  \  { z } )  ->  ( ( B  e.  Fin  ->  (
x  X.  B )  e.  Fin )  <->  ( B  e.  Fin  ->  ( (
y  \  { z } )  X.  B
)  e.  Fin )
) )
7 xpeq1 4859 . . . . 5  |-  ( x  =  y  ->  (
x  X.  B )  =  ( y  X.  B ) )
87eleq1d 2509 . . . 4  |-  ( x  =  y  ->  (
( x  X.  B
)  e.  Fin  <->  ( y  X.  B )  e.  Fin ) )
98imbi2d 316 . . 3  |-  ( x  =  y  ->  (
( B  e.  Fin  ->  ( x  X.  B
)  e.  Fin )  <->  ( B  e.  Fin  ->  ( y  X.  B )  e.  Fin ) ) )
10 xpeq1 4859 . . . . 5  |-  ( x  =  A  ->  (
x  X.  B )  =  ( A  X.  B ) )
1110eleq1d 2509 . . . 4  |-  ( x  =  A  ->  (
( x  X.  B
)  e.  Fin  <->  ( A  X.  B )  e.  Fin ) )
1211imbi2d 316 . . 3  |-  ( x  =  A  ->  (
( B  e.  Fin  ->  ( x  X.  B
)  e.  Fin )  <->  ( B  e.  Fin  ->  ( A  X.  B )  e.  Fin ) ) )
13 0xp 4922 . . . . 5  |-  ( (/)  X.  B )  =  (/)
14 0fin 7545 . . . . 5  |-  (/)  e.  Fin
1513, 14eqeltri 2513 . . . 4  |-  ( (/)  X.  B )  e.  Fin
1615a1i 11 . . 3  |-  ( B  e.  Fin  ->  ( (/) 
X.  B )  e. 
Fin )
17 neq0 3652 . . . . . . 7  |-  ( -.  y  =  (/)  <->  E. w  w  e.  y )
18 sneq 3892 . . . . . . . . . . . . . . . 16  |-  ( z  =  w  ->  { z }  =  { w } )
1918difeq2d 3479 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  (
y  \  { z } )  =  ( y  \  { w } ) )
2019xpeq1d 4868 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  (
( y  \  {
z } )  X.  B )  =  ( ( y  \  {
w } )  X.  B ) )
2120eleq1d 2509 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
( ( y  \  { z } )  X.  B )  e. 
Fin 
<->  ( ( y  \  { w } )  X.  B )  e. 
Fin ) )
2221imbi2d 316 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( B  e.  Fin  ->  ( ( y  \  { z } )  X.  B )  e. 
Fin )  <->  ( B  e.  Fin  ->  ( (
y  \  { w } )  X.  B
)  e.  Fin )
) )
2322rspcv 3074 . . . . . . . . . . 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 466 . . . . . . . . . 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 39 . . . . . . . . . . 11  |-  ( B  e.  Fin  ->  (
( B  e.  Fin  ->  ( ( y  \  { w } )  X.  B )  e. 
Fin )  ->  (
( y  \  {
w } )  X.  B )  e.  Fin ) )
2625ad2antlr 726 . . . . . . . . . 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 4538 . . . . . . . . . . . . . . 15  |-  { w }  e.  _V
28 xpexg 6512 . . . . . . . . . . . . . . 15  |-  ( ( { w }  e.  _V  /\  B  e.  Fin )  ->  ( { w }  X.  B )  e. 
_V )
2927, 28mpan 670 . . . . . . . . . . . . . 14  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  e.  _V )
30 id 22 . . . . . . . . . . . . . 14  |-  ( B  e.  Fin  ->  B  e.  Fin )
31 vex 2980 . . . . . . . . . . . . . . 15  |-  w  e. 
_V
32 2ndconst 6667 . . . . . . . . . . . . . . 15  |-  ( w  e.  _V  ->  ( 2nd  |`  ( { w }  X.  B ) ) : ( { w }  X.  B ) -1-1-onto-> B )
3331, 32mp1i 12 . . . . . . . . . . . . . 14  |-  ( B  e.  Fin  ->  ( 2nd  |`  ( { w }  X.  B ) ) : ( { w }  X.  B ) -1-1-onto-> B )
34 f1oen2g 7331 . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . 13  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  ~~  B
)
36 enfii 7535 . . . . . . . . . . . . 13  |-  ( ( B  e.  Fin  /\  ( { w }  X.  B )  ~~  B
)  ->  ( {
w }  X.  B
)  e.  Fin )
3735, 36mpdan 668 . . . . . . . . . . . 12  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  e.  Fin )
3837ad2antlr 726 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( {
w }  X.  B
)  e.  Fin )
39 unfi 7584 . . . . . . . . . . . 12  |-  ( ( ( ( y  \  { w } )  X.  B )  e. 
Fin  /\  ( {
w }  X.  B
)  e.  Fin )  ->  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin )
40 xpundir 4897 . . . . . . . . . . . . . . . 16  |-  ( ( ( y  \  {
w } )  u. 
{ w } )  X.  B )  =  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )
41 difsnid 4024 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  y  ->  (
( y  \  {
w } )  u. 
{ w } )  =  y )
4241xpeq1d 4868 . . . . . . . . . . . . . . . 16  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  u.  { w }
)  X.  B )  =  ( y  X.  B ) )
4340, 42syl5eqr 2489 . . . . . . . . . . . . . . 15  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  X.  B )  u.  ( { w }  X.  B ) )  =  ( y  X.  B
) )
4443eleq1d 2509 . . . . . . . . . . . . . 14  |-  ( w  e.  y  ->  (
( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin  <->  ( y  X.  B )  e.  Fin ) )
4544biimpd 207 . . . . . . . . . . . . 13  |-  ( w  e.  y  ->  (
( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin  ->  (
y  X.  B )  e.  Fin ) )
4645adantl 466 . . . . . . . . . . . 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 32 . . . . . . . . . . 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 674 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\  B  e.  Fin )  /\  w  e.  y
)  ->  ( (
( y  \  {
w } )  X.  B )  e.  Fin  ->  ( y  X.  B
)  e.  Fin )
)
4924, 26, 483syld 55 . . . . . . . . 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 434 . . . . . . . 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 1690 . . . . . . 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 217 . . . . . 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 4859 . . . . . . . 8  |-  ( y  =  (/)  ->  ( y  X.  B )  =  ( (/)  X.  B
) )
5453, 15syl6eqel 2531 . . . . . . 7  |-  ( y  =  (/)  ->  ( y  X.  B )  e. 
Fin )
5554a1d 25 . . . . . 6  |-  ( y  =  (/)  ->  ( A. z  e.  y  ( B  e.  Fin  ->  (
( y  \  {
z } )  X.  B )  e.  Fin )  ->  ( y  X.  B )  e.  Fin ) )
5652, 55pm2.61d2 160 . . . . 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 434 . . . 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 78 . . 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 7556 . 2  |-  ( A  e.  Fin  ->  ( B  e.  Fin  ->  ( A  X.  B )  e. 
Fin ) )
6059imp 429 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 369    = wceq 1369   E.wex 1586    e. wcel 1756   A.wral 2720   _Vcvv 2977    \ cdif 3330    u. cun 3331   (/)c0 3642   {csn 3882   class class class wbr 4297    X. cxp 4843    |` cres 4847   -1-1-onto->wf1o 5422   2ndc2nd 6581    ~~ cen 7312   Fincfn 7315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-reu 2727  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-uni 4097  df-int 4134  df-iun 4178  df-br 4298  df-opab 4356  df-mpt 4357  df-tr 4391  df-eprel 4637  df-id 4641  df-po 4646  df-so 4647  df-fr 4684  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-om 6482  df-1st 6582  df-2nd 6583  df-recs 6837  df-rdg 6871  df-1o 6925  df-oadd 6929  df-er 7106  df-en 7316  df-fin 7319
This theorem is referenced by:  mapfi  7612  fsuppxpfi  7642  infxpenlem  8185  ackbij1lem9  8402  ackbij1lem10  8403  hashxplem  12200  hashmap  12202  fsum2dlem  13242  fsumcom2  13246  ackbijnn  13296  rexpen  13515  crt  13858  phimullem  13859  prmreclem3  13984  ablfaclem3  16593  gsumdixpOLD  16705  gsumdixp  16706  gsumbagdiag  17451  psrass1lem  17452  mplsubrglemOLD  17523  evlslem2  17602  frlmbas3  18206  mamudm  18293  mamufacex  18294  mamures  18295  gsumcom3fi  18305  mamucl  18306  mamudiagcl  18307  mamudi  18312  mamudir  18313  mamuvs1  18314  mamuvs2  18315  matsca2  18326  matbas2  18327  matplusg2  18332  matvsca2  18333  mattposcl  18342  mdetrsca  18415  mdetunilem9  18431  tsmsxplem1  19732  tsmsxplem2  19733  tsmsxp  19734  i1fadd  21178  i1fmul  21179  itg1addlem4  21182  fsumdvdsmul  22540  fsumvma  22557  lgsquadlem1  22698  lgsquadlem2  22699  lgsquadlem3  22700  relfi  25945  sibfof  26731  erdszelem10  27093  fprod2dlem  27496  fprodcom2  27500  cntotbnd  28700  pellex  29181  3xpfi  30171  2spotfi  30416  matplusgcell  30864  matsubgcell  30865  matvscacell  30866  matgsum  30867  pmatcoe1fsupp  30897
  Copyright terms: Public domain W3C validator