Theorem xpfi 9269

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

Assertion

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

Proof of Theorem xpfi

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ∪ cun 3912   ⊆ wss 3914  𝒫 cpw 4563   × cxp 5636  Fincfn 8918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-om 7843  df-1o 8434  df-en 8919  df-dom 8920  df-fin 8922

This theorem is referenced by:  3xpfi  9271  fodomfir  9279  mapfi  9299  fsuppxpfi  9336  infxpenlem  9966  ficardadju  10153  ackbij1lem9  10180  ackbij1lem10  10181  hashxplem  14398  hashmap  14400  fsum2dlem  15736  fsumcom2  15740  ackbijnn  15794  fprod2dlem  15946  fprodcom2  15950  rexpen  16196  crth  16748  phimullem  16749  prmreclem3  16889  gsumcom3fi  19909  ablfaclem3  20019  gsumdixp  20228  frlmbas3  21685  gsumbagdiag  21840  psrass1lem  21841  evlslem2  21986  mamudm  22282  mamufacex  22283  mamures  22284  mamucl  22288  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  matsca2  22307  matbas2  22308  matplusg2  22314  matvsca2  22315  matplusgcell  22320  matsubgcell  22321  matvscacell  22323  matgsum  22324  mamumat1cl  22326  mattposcl  22340  mdetrsca  22490  mdetunilem9  22507  pmatcoe1fsupp  22588  tsmsxplem1  24040  tsmsxplem2  24041  tsmsxp  24042  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  fsumvma  27124  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  madefi  27824  relfi  32531  fsumiunle  32754  elrgspnlem2  33194  matdim  33611  fedgmullem1  33625  fldextrspunlsplem  33668  sibfof  34331  hgt750lemb  34647  erdszelem10  35187  matunitlindflem2  37611  matunitlindf  37612  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  cntotbnd  37790  aks6d1c2  42118  sticksstones22  42156  pellex  42823  mnringmulrcld  44217  fourierdlem42  46147  etransclem44  46276  etransclem45  46277  etransclem47  46279