Theorem xpfi 9220

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

Assertion

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

Proof of Theorem xpfi

Step	Hyp	Ref	Expression
1		unfi 9095	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
2		pwfi 9219	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
3		pwfi 9219	. . . 4 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
4	2, 3	bitri 276	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
5	1, 4	sylib 219	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin)
6		xpsspw 5752	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
7		ssfi 9097	. 2 ⊢ ((𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ∈ Fin)
8	5, 6, 7	sylancl 592	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ∪ cun 3881   ⊆ wss 3883  𝒫 cpw 4529   × cxp 5616  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-om 7807  df-1o 8395  df-en 8884  df-dom 8885  df-fin 8887

This theorem is referenced by:  3xpfi  9221  fodomfir  9228  mapfi  9248  fsuppxpfi  9288  infxpenlem  9926  ficardadju  10113  ackbij1lem9  10140  ackbij1lem10  10141  hashxplem  14386  hashmap  14388  fsum2dlem  15723  fsumcom2  15727  ackbijnn  15784  fprod2dlem  15936  fprodcom2  15940  rexpen  16186  crth  16739  phimullem  16740  prmreclem3  16880  gsumcom3fi  19945  ablfaclem3  20055  gsumdixp  20289  frlmbas3  21751  gsumbagdiag  21907  psrass1lem  21908  evlslem2  22055  mamudm  22378  mamufacex  22379  mamures  22380  mamucl  22384  mamudi  22386  mamudir  22387  mamuvs1  22388  mamuvs2  22389  matsca2  22403  matbas2  22404  matplusg2  22410  matvsca2  22411  matplusgcell  22416  matsubgcell  22417  matvscacell  22419  matgsum  22420  mamumat1cl  22422  mattposcl  22436  mdetrsca  22586  mdetunilem9  22603  pmatcoe1fsupp  22684  tsmsxplem1  24136  tsmsxplem2  24137  tsmsxp  24138  i1fadd  25680  i1fmul  25681  itg1addlem4  25684  fsumdvdsmul  27176  fsumvma  27194  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  madefi  27923  relfi  32691  fsumiunle  32921  elrgspnlem2  33324  matdim  33799  fedgmullem1  33813  fldextrspunlsplem  33857  sibfof  34524  hgt750lemb  34840  erdszelem10  35428  matunitlindflem2  37984  matunitlindf  37985  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  cntotbnd  38163  aks6d1c2  42615  sticksstones22  42653  pellex  43280  mnringmulrcld  44672  fourierdlem42  46592  etransclem44  46721  etransclem45  46722  etransclem47  46724