Theorem xpfi 9232

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 5312. (Revised by BTernaryTau, 10-Jan-2025.)

Assertion

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

Proof of Theorem xpfi

Step	Hyp	Ref	Expression
1		unfi 9107	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
2		pwfi 9231	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
3		pwfi 9231	. . . 4 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
4	2, 3	bitri 275	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
5	1, 4	sylib 218	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
6		xpsspw 5766	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
7		ssfi 9109	. 2 ⊢ ((𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ∈ Fin)
8	5, 6, 7	sylancl 587	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ∪ cun 3901   ⊆ wss 3903  𝒫 cpw 4556   × cxp 5630  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-om 7819  df-1o 8407  df-en 8896  df-dom 8897  df-fin 8899

This theorem is referenced by:  3xpfi  9233  fodomfir  9240  mapfi  9260  fsuppxpfi  9300  infxpenlem  9935  ficardadju  10122  ackbij1lem9  10149  ackbij1lem10  10150  hashxplem  14368  hashmap  14370  fsum2dlem  15705  fsumcom2  15709  ackbijnn  15763  fprod2dlem  15915  fprodcom2  15919  rexpen  16165  crth  16717  phimullem  16718  prmreclem3  16858  gsumcom3fi  19920  ablfaclem3  20030  gsumdixp  20266  frlmbas3  21743  gsumbagdiag  21899  psrass1lem  21900  evlslem2  22046  mamudm  22351  mamufacex  22352  mamures  22353  mamucl  22357  mamudi  22359  mamudir  22360  mamuvs1  22361  mamuvs2  22362  matsca2  22376  matbas2  22377  matplusg2  22383  matvsca2  22384  matplusgcell  22389  matsubgcell  22390  matvscacell  22392  matgsum  22393  mamumat1cl  22395  mattposcl  22409  mdetrsca  22559  mdetunilem9  22576  pmatcoe1fsupp  22657  tsmsxplem1  24109  tsmsxplem2  24110  tsmsxp  24111  i1fadd  25664  i1fmul  25665  itg1addlem4  25668  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  fsumvma  27192  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  madefi  27921  relfi  32689  fsumiunle  32921  elrgspnlem2  33337  matdim  33793  fedgmullem1  33807  fldextrspunlsplem  33851  sibfof  34518  hgt750lemb  34834  erdszelem10  35416  matunitlindflem2  37868  matunitlindf  37869  poimirlem26  37897  poimirlem27  37898  poimirlem28  37899  cntotbnd  38047  aks6d1c2  42500  sticksstones22  42538  pellex  43192  mnringmulrcld  44584  fourierdlem42  46507  etransclem44  46636  etransclem45  46637  etransclem47  46639