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

Theorem xpfi 7787
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 5013 . . . . 5  |-  ( x  =  (/)  ->  ( x  X.  B )  =  ( (/)  X.  B
) )
21eleq1d 2536 . . . 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 5013 . . . . 5  |-  ( x  =  ( y  \  { z } )  ->  ( x  X.  B )  =  ( ( y  \  {
z } )  X.  B ) )
54eleq1d 2536 . . . 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 5013 . . . . 5  |-  ( x  =  y  ->  (
x  X.  B )  =  ( y  X.  B ) )
87eleq1d 2536 . . . 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 5013 . . . . 5  |-  ( x  =  A  ->  (
x  X.  B )  =  ( A  X.  B ) )
1110eleq1d 2536 . . . 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 5078 . . . . 5  |-  ( (/)  X.  B )  =  (/)
14 0fin 7744 . . . . 5  |-  (/)  e.  Fin
1513, 14eqeltri 2551 . . . 4  |-  ( (/)  X.  B )  e.  Fin
1615a1i 11 . . 3  |-  ( B  e.  Fin  ->  ( (/) 
X.  B )  e. 
Fin )
17 neq0 3795 . . . . . . 7  |-  ( -.  y  =  (/)  <->  E. w  w  e.  y )
18 sneq 4037 . . . . . . . . . . . . . . . 16  |-  ( z  =  w  ->  { z }  =  { w } )
1918difeq2d 3622 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  (
y  \  { z } )  =  ( y  \  { w } ) )
2019xpeq1d 5022 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  (
( y  \  {
z } )  X.  B )  =  ( ( y  \  {
w } )  X.  B ) )
2120eleq1d 2536 . . . . . . . . . . . . 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 3210 . . . . . . . . . . 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 4688 . . . . . . . . . . . . . . 15  |-  { w }  e.  _V
28 xpexg 6709 . . . . . . . . . . . . . . 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 3116 . . . . . . . . . . . . . . 15  |-  w  e. 
_V
32 2ndconst 6869 . . . . . . . . . . . . . . 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 7529 . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . 13  |-  ( B  e.  Fin  ->  ( { w }  X.  B )  ~~  B
)
36 enfii 7734 . . . . . . . . . . . . 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 7783 . . . . . . . . . . . 12  |-  ( ( ( ( y  \  { w } )  X.  B )  e. 
Fin  /\  ( {
w }  X.  B
)  e.  Fin )  ->  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )  e.  Fin )
40 xpundir 5052 . . . . . . . . . . . . . . . 16  |-  ( ( ( y  \  {
w } )  u. 
{ w } )  X.  B )  =  ( ( ( y 
\  { w }
)  X.  B )  u.  ( { w }  X.  B ) )
41 difsnid 4173 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  y  ->  (
( y  \  {
w } )  u. 
{ w } )  =  y )
4241xpeq1d 5022 . . . . . . . . . . . . . . . 16  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  u.  { w }
)  X.  B )  =  ( y  X.  B ) )
4340, 42syl5eqr 2522 . . . . . . . . . . . . . . 15  |-  ( w  e.  y  ->  (
( ( y  \  { w } )  X.  B )  u.  ( { w }  X.  B ) )  =  ( y  X.  B
) )
4443eleq1d 2536 . . . . . . . . . . . . . 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 1700 . . . . . . 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 5013 . . . . . . . 8  |-  ( y  =  (/)  ->  ( y  X.  B )  =  ( (/)  X.  B
) )
5453, 15syl6eqel 2563 . . . . . . 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 7755 . 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 1379   E.wex 1596    e. wcel 1767   A.wral 2814   _Vcvv 3113    \ cdif 3473    u. cun 3474   (/)c0 3785   {csn 4027   class class class wbr 4447    X. cxp 4997    |` cres 5001   -1-1-onto->wf1o 5585   2ndc2nd 6780    ~~ cen 7510   Fincfn 7513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-en 7514  df-fin 7517
This theorem is referenced by:  3xpfi  7788  mapfi  7812  fsuppxpfi  7842  infxpenlem  8387  ackbij1lem9  8604  ackbij1lem10  8605  hashxplem  12453  hashmap  12455  fsum2dlem  13544  fsumcom2  13548  ackbijnn  13599  rexpen  13818  crt  14163  phimullem  14164  prmreclem3  14291  ablfaclem3  16928  gsumdixpOLD  17041  gsumdixp  17042  gsumbagdiag  17799  psrass1lem  17800  mplsubrglemOLD  17872  evlslem2  17951  frlmbas3  18574  mamudm  18657  mamufacex  18658  mamures  18659  gsumcom3fi  18669  mamucl  18670  mamudi  18672  mamudir  18673  mamuvs1  18674  mamuvs2  18675  matsca2  18689  matbas2  18690  matplusg2  18696  matvsca2  18697  matplusgcell  18702  matsubgcell  18703  matvscacell  18705  matgsum  18706  mamumat1cl  18708  mattposcl  18722  mdetrsca  18872  mdetunilem9  18889  pmatcoe1fsupp  18969  tsmsxplem1  20390  tsmsxplem2  20391  tsmsxp  20392  i1fadd  21837  i1fmul  21838  itg1addlem4  21841  fsumdvdsmul  23199  fsumvma  23216  lgsquadlem1  23357  lgsquadlem2  23358  lgsquadlem3  23359  2spotfi  24568  relfi  27132  sibfof  27922  erdszelem10  28284  fprod2dlem  28687  fprodcom2  28691  cntotbnd  29895  pellex  30375  fourierdlem42  31449
  Copyright terms: Public domain W3C validator