Theorem xpfi 9258

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

Assertion

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

Proof of Theorem xpfi

Step	Hyp	Ref	Expression
1		unfi 9133	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
2		pwfi 9257	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
3		pwfi 9257	. . . 4 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
4	2, 3	bitri 277	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
5	1, 4	sylib 220	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
6		xpsspw 5778	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
7		ssfi 9135	. 2 ⊢ ((𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ∈ Fin)
8	5, 6, 7	sylancl 595	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   ∪ cun 3900   ⊆ wss 3902  𝒫 cpw 4552   × cxp 5641  Fincfn 8921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-om 7842  df-1o 8431  df-en 8922  df-dom 8923  df-fin 8925

This theorem is referenced by:  3xpfi  9259  fodomfir  9266  mapfi  9285  fsuppxpfi  9325  infxpenlem  9963  ficardadju  10150  ackbij1lem9  10177  ackbij1lem10  10178  hashxplem  14440  hashmap  14442  fsum2dlem  15788  fsumcom2  15792  ackbijnn  15849  fprod2dlem  16001  fprodcom2  16005  rexpen  16251  crth  16804  phimullem  16805  prmreclem3  16945  gsumcom3fi  20010  ablfaclem3  20120  gsumdixp  20354  frlmbas3  21816  gsumbagdiag  21972  psrass1lem  21973  evlslem2  22120  mamudm  22443  mamufacex  22444  mamures  22445  mamucl  22449  mamudi  22451  mamudir  22452  mamuvs1  22453  mamuvs2  22454  matsca2  22468  matbas2  22469  matplusg2  22475  matvsca2  22476  matplusgcell  22481  matsubgcell  22482  matvscacell  22484  matgsum  22485  mamumat1cl  22487  mattposcl  22501  mdetrsca  22651  mdetunilem9  22668  pmatcoe1fsupp  22749  tsmsxplem1  24201  tsmsxplem2  24202  tsmsxp  24203  i1fadd  25745  i1fmul  25746  itg1addlem4  25749  fsumdvdsmul  27247  fsumvma  27265  lgsquadlem1  27432  lgsquadlem2  27433  lgsquadlem3  27434  madefi  27994  relfi  32762  fsumiunle  32992  elrgspnlem2  33385  matdim  33873  fedgmullem1  33887  fldextrspunlsplem  33931  sibfof  34598  hgt750lemb  34911  erdszelem10  35511  matunitlindflem2  38077  matunitlindf  38078  poimirlem26  38106  poimirlem27  38107  poimirlem28  38108  cntotbnd  38256  aks6d1c2  42708  sticksstones22  42746  pellex  43373  mnringmulrcld  44765  fourierdlem42  46684  etransclem44  46813  etransclem45  46814  etransclem47  46816