Theorem xpfi 9275

Description: The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5334. (Revised by BTernaryTau, 10-Jan-2025.)

Assertion

Ref	Expression
xpfi	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Proof of Theorem xpfi

Step	Hyp	Ref	Expression
1		unfi 9151	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
2		pwfi 9274	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
3		pwfi 9274	. . . 4 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
4	2, 3	bitri 278	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
5	1, 4	sylib 221	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
6		xpsspw 5794	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
7		ssfi 9153	. 2 ⊢ ((𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ∈ Fin)
8	5, 6, 7	sylancl 597	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ∪ cun 3911   ⊆ wss 3913  𝒫 cpw 4564   × cxp 5657  Fincfn 8939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-om 7859  df-1o 8449  df-en 8940  df-dom 8941  df-fin 8943

This theorem is referenced by:  3xpfi  9276  fodomfir  9283  mapfi  9301  fsuppxpfi  9341  infxpenlem  9993  ficardadju  10179  ackbij1lem9  10206  ackbij1lem10  10207  hashxplem  14466  hashmap  14468  fsum2dlem  15817  fsumcom2  15821  ackbijnn  15878  fprod2dlem  16030  fprodcom2  16034  rexpen  16280  crth  16833  phimullem  16834  prmreclem3  16974  gsumcom3fi  20045  ablfaclem3  20155  gsumdixp  20396  frlmbas3  21891  gsumbagdiag  22047  psrass1lem  22048  evlslem2  22195  mamudm  22517  mamufacex  22518  mamures  22519  mamucl  22523  mamudi  22525  mamudir  22526  mamuvs1  22527  mamuvs2  22528  matsca2  22542  matbas2  22543  matplusg2  22549  matvsca2  22550  matplusgcell  22555  matsubgcell  22556  matvscacell  22558  matgsum  22559  mamumat1cl  22561  mattposcl  22575  mdetrsca  22725  mdetunilem9  22742  pmatcoe1fsupp  22823  tsmsxplem1  24275  tsmsxplem2  24276  tsmsxp  24277  i1fadd  25819  i1fmul  25820  itg1addlem4  25823  fsumdvdsmul  27321  fsumvma  27339  lgsquadlem1  27506  lgsquadlem2  27507  lgsquadlem3  27508  madefi  28068  relfi  32884  fsumiunle  33110  elrgspnlem2  33500  matdim  33946  fedgmullem1  33960  fldextrspunlsplem  34004  sibfof  34671  hgt750lemb  34984  erdszelem10  35587  matunitlindflem2  38151  matunitlindf  38152  poimirlem26  38180  poimirlem27  38181  poimirlem28  38182  cntotbnd  38330  aks6d1c2  42782  sticksstones22  42820  pellex  43449  mnringmulrcld  44839  fourierdlem42  46750  etransclem44  46879  etransclem45  46880  etransclem47  46882