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

Theorem xpfi 7793
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 5003 . . . . 5  |-  ( x  =  (/)  ->  ( x  X.  B )  =  ( (/)  X.  B
) )
21eleq1d 2512 . . . 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 5003 . . . . 5  |-  ( x  =  ( y  \  { z } )  ->  ( x  X.  B )  =  ( ( y  \  {
z } )  X.  B ) )
54eleq1d 2512 . . . 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 5003 . . . . 5  |-  ( x  =  y  ->  (
x  X.  B )  =  ( y  X.  B ) )
87eleq1d 2512 . . . 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 5003 . . . . 5  |-  ( x  =  A  ->  (
x  X.  B )  =  ( A  X.  B ) )
1110eleq1d 2512 . . . 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 5070 . . . . 5  |-  ( (/)  X.  B )  =  (/)
14 0fin 7749 . . . . 5  |-  (/)  e.  Fin
1513, 14eqeltri 2527 . . . 4  |-  ( (/)  X.  B )  e.  Fin
1615a1i 11 . . 3  |-  ( B  e.  Fin  ->  ( (/) 
X.  B )  e. 
Fin )
17 neq0 3781 . . . . . . 7  |-  ( -.  y  =  (/)  <->  E. w  w  e.  y )
18 sneq 4024 . . . . . . . . . . . . . . . 16  |-  ( z  =  w  ->  { z }  =  { w } )
1918difeq2d 3607 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  (
y  \  { z } )  =  ( y  \  { w } ) )
2019xpeq1d 5012 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  (
( y  \  {
z } )  X.  B )  =  ( ( y  \  {
w } )  X.  B ) )
2120eleq1d 2512 . . . . . . . . . . . . 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 3192 . . . . . . . . . . 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 4678 . . . . . . . . . . . . . . 15  |-  { w }  e.  _V
28 xpexg 6587 . . . . . . . . . . . . . . 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 3098 . . . . . . . . . . . . . . 15  |-  w  e. 
_V
32 2ndconst 6874 . . . . . . . . . . . . . . 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 7534 . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . 13  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  ~~  B
)
36 enfii 7739 . . . . . . . . . . . . 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 7789 . . . . . . . . . . . 12  |-  ( ( ( ( y  \  { w } )  X.  B )  e. 
Fin  /\  ( {
w }  X.  B
)  e.  Fin )  ->  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin )
40 xpundir 5043 . . . . . . . . . . . . . . . 16  |-  ( ( ( y  \  {
w } )  u. 
{ w } )  X.  B )  =  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )
41 difsnid 4161 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  y  ->  (
( y  \  {
w } )  u. 
{ w } )  =  y )
4241xpeq1d 5012 . . . . . . . . . . . . . . . 16  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  u.  { w }
)  X.  B )  =  ( y  X.  B ) )
4340, 42syl5eqr 2498 . . . . . . . . . . . . . . 15  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  X.  B )  u.  ( { w }  X.  B ) )  =  ( y  X.  B
) )
4443eleq1d 2512 . . . . . . . . . . . . . 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 1711 . . . . . . 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 5003 . . . . . . . 8  |-  ( y  =  (/)  ->  ( y  X.  B )  =  ( (/)  X.  B
) )
5453, 15syl6eqel 2539 . . . . . . 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 7761 . 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 1383   E.wex 1599    e. wcel 1804   A.wral 2793   _Vcvv 3095    \ cdif 3458    u. cun 3459   (/)c0 3770   {csn 4014   class class class wbr 4437    X. cxp 4987    |` cres 4991   -1-1-onto->wf1o 5577   2ndc2nd 6784    ~~ cen 7515   Fincfn 7518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-en 7519  df-fin 7522
This theorem is referenced by:  3xpfi  7794  mapfi  7818  fsuppxpfi  7848  infxpenlem  8394  ackbij1lem9  8611  ackbij1lem10  8612  hashxplem  12470  hashmap  12472  fsum2dlem  13564  fsumcom2  13568  ackbijnn  13619  rexpen  13838  crt  14185  phimullem  14186  prmreclem3  14313  ablfaclem3  17012  gsumdixpOLD  17131  gsumdixp  17132  gsumbagdiag  17902  psrass1lem  17903  mplsubrglemOLD  17975  evlslem2  18054  frlmbas3  18680  mamudm  18763  mamufacex  18764  mamures  18765  gsumcom3fi  18775  mamucl  18776  mamudi  18778  mamudir  18779  mamuvs1  18780  mamuvs2  18781  matsca2  18795  matbas2  18796  matplusg2  18802  matvsca2  18803  matplusgcell  18808  matsubgcell  18809  matvscacell  18811  matgsum  18812  mamumat1cl  18814  mattposcl  18828  mdetrsca  18978  mdetunilem9  18995  pmatcoe1fsupp  19075  tsmsxplem1  20528  tsmsxplem2  20529  tsmsxp  20530  i1fadd  21975  i1fmul  21976  itg1addlem4  21979  fsumdvdsmul  23343  fsumvma  23360  lgsquadlem1  23501  lgsquadlem2  23502  lgsquadlem3  23503  relfi  27331  sibfof  28155  erdszelem10  28517  fprod2dlem  29085  fprodcom2  29089  cntotbnd  30267  pellex  30746  fourierdlem42  31820
  Copyright terms: Public domain W3C validator