Theorem xpfi 9199

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

Assertion

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

Proof of Theorem xpfi

Step	Hyp	Ref	Expression
1		unfi 9075	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
2		pwfi 9198	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
3		pwfi 9198	. . . 4 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
4	2, 3	bitri 275	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
5	1, 4	sylib 218	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
6		xpsspw 5744	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
7		ssfi 9077	. 2 ⊢ ((𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ∈ Fin)
8	5, 6, 7	sylancl 586	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ∪ cun 3895   ⊆ wss 3897  𝒫 cpw 4545   × cxp 5609  Fincfn 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-om 7792  df-1o 8380  df-en 8865  df-dom 8866  df-fin 8868

This theorem is referenced by:  3xpfi  9200  fodomfir  9207  mapfi  9227  fsuppxpfi  9264  infxpenlem  9899  ficardadju  10086  ackbij1lem9  10113  ackbij1lem10  10114  hashxplem  14335  hashmap  14337  fsum2dlem  15672  fsumcom2  15676  ackbijnn  15730  fprod2dlem  15882  fprodcom2  15886  rexpen  16132  crth  16684  phimullem  16685  prmreclem3  16825  gsumcom3fi  19886  ablfaclem3  19996  gsumdixp  20232  frlmbas3  21708  gsumbagdiag  21863  psrass1lem  21864  evlslem2  22009  mamudm  22305  mamufacex  22306  mamures  22307  mamucl  22311  mamudi  22313  mamudir  22314  mamuvs1  22315  mamuvs2  22316  matsca2  22330  matbas2  22331  matplusg2  22337  matvsca2  22338  matplusgcell  22343  matsubgcell  22344  matvscacell  22346  matgsum  22347  mamumat1cl  22349  mattposcl  22363  mdetrsca  22513  mdetunilem9  22530  pmatcoe1fsupp  22611  tsmsxplem1  24063  tsmsxplem2  24064  tsmsxp  24065  i1fadd  25618  i1fmul  25619  itg1addlem4  25622  fsumdvdsmul  27127  fsumdvdsmulOLD  27129  fsumvma  27146  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  madefi  27853  relfi  32574  fsumiunle  32804  elrgspnlem2  33202  matdim  33620  fedgmullem1  33634  fldextrspunlsplem  33678  sibfof  34345  hgt750lemb  34661  erdszelem10  35236  matunitlindflem2  37657  matunitlindf  37658  poimirlem26  37686  poimirlem27  37687  poimirlem28  37688  cntotbnd  37836  aks6d1c2  42163  sticksstones22  42201  pellex  42868  mnringmulrcld  44261  fourierdlem42  46187  etransclem44  46316  etransclem45  46317  etransclem47  46319