MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpfi Structured version   Visualization version   GIF version

Theorem xpfi 8781
Description: The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)
Assertion
Ref Expression
xpfi ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Proof of Theorem xpfi
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpeq1 5567 . . . . 5 (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵))
21eleq1d 2901 . . . 4 (𝑥 = ∅ → ((𝑥 × 𝐵) ∈ Fin ↔ (∅ × 𝐵) ∈ Fin))
32imbi2d 342 . . 3 (𝑥 = ∅ → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)))
4 xpeq1 5567 . . . . 5 (𝑥 = (𝑦 ∖ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∖ {𝑧}) × 𝐵))
54eleq1d 2901 . . . 4 (𝑥 = (𝑦 ∖ {𝑧}) → ((𝑥 × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin))
65imbi2d 342 . . 3 (𝑥 = (𝑦 ∖ {𝑧}) → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin)))
7 xpeq1 5567 . . . . 5 (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵))
87eleq1d 2901 . . . 4 (𝑥 = 𝑦 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
98imbi2d 342 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
10 xpeq1 5567 . . . . 5 (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵))
1110eleq1d 2901 . . . 4 (𝑥 = 𝐴 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝐴 × 𝐵) ∈ Fin))
1211imbi2d 342 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin)))
13 0xp 5647 . . . . 5 (∅ × 𝐵) = ∅
14 0fin 8738 . . . . 5 ∅ ∈ Fin
1513, 14eqeltri 2913 . . . 4 (∅ × 𝐵) ∈ Fin
1615a1i 11 . . 3 (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)
17 neq0 4312 . . . . . . 7 𝑦 = ∅ ↔ ∃𝑤 𝑤𝑦)
18 sneq 4573 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → {𝑧} = {𝑤})
1918difeq2d 4102 . . . . . . . . . . . . . . 15 (𝑧 = 𝑤 → (𝑦 ∖ {𝑧}) = (𝑦 ∖ {𝑤}))
2019xpeq1d 5582 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → ((𝑦 ∖ {𝑧}) × 𝐵) = ((𝑦 ∖ {𝑤}) × 𝐵))
2120eleq1d 2901 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
2221imbi2d 342 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
2322rspcv 3621 . . . . . . . . . . 11 (𝑤𝑦 → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
2423adantl 482 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
25 pm2.27 42 . . . . . . . . . . 11 (𝐵 ∈ Fin → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin) → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
2625ad2antlr 723 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin) → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
27 snex 5327 . . . . . . . . . . . . . . 15 {𝑤} ∈ V
28 xpexg 7465 . . . . . . . . . . . . . . 15 (({𝑤} ∈ V ∧ 𝐵 ∈ Fin) → ({𝑤} × 𝐵) ∈ V)
2927, 28mpan 686 . . . . . . . . . . . . . 14 (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ V)
30 id 22 . . . . . . . . . . . . . 14 (𝐵 ∈ Fin → 𝐵 ∈ Fin)
31 vex 3502 . . . . . . . . . . . . . . 15 𝑤 ∈ V
32 2ndconst 7790 . . . . . . . . . . . . . . 15 (𝑤 ∈ V → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto𝐵)
3331, 32mp1i 13 . . . . . . . . . . . . . 14 (𝐵 ∈ Fin → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto𝐵)
34 f1oen2g 8518 . . . . . . . . . . . . . 14 ((({𝑤} × 𝐵) ∈ V ∧ 𝐵 ∈ Fin ∧ (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto𝐵) → ({𝑤} × 𝐵) ≈ 𝐵)
3529, 30, 33, 34syl3anc 1365 . . . . . . . . . . . . 13 (𝐵 ∈ Fin → ({𝑤} × 𝐵) ≈ 𝐵)
36 enfii 8727 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ ({𝑤} × 𝐵) ≈ 𝐵) → ({𝑤} × 𝐵) ∈ Fin)
3735, 36mpdan 683 . . . . . . . . . . . 12 (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ Fin)
3837ad2antlr 723 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ({𝑤} × 𝐵) ∈ Fin)
39 unfi 8777 . . . . . . . . . . . 12 ((((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin ∧ ({𝑤} × 𝐵) ∈ Fin) → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin)
40 xpundir 5619 . . . . . . . . . . . . . . . 16 (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵))
41 difsnid 4741 . . . . . . . . . . . . . . . . 17 (𝑤𝑦 → ((𝑦 ∖ {𝑤}) ∪ {𝑤}) = 𝑦)
4241xpeq1d 5582 . . . . . . . . . . . . . . . 16 (𝑤𝑦 → (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (𝑦 × 𝐵))
4340, 42syl5eqr 2874 . . . . . . . . . . . . . . 15 (𝑤𝑦 → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) = (𝑦 × 𝐵))
4443eleq1d 2901 . . . . . . . . . . . . . 14 (𝑤𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
4544biimpd 230 . . . . . . . . . . . . 13 (𝑤𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
4645adantl 482 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
4739, 46syl5 34 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ((((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin ∧ ({𝑤} × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
4838, 47mpan2d 690 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → (((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
4924, 26, 483syld 60 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
5049ex 413 . . . . . . . 8 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑤𝑦 → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
5150exlimdv 1927 . . . . . . 7 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑤 𝑤𝑦 → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
5217, 51syl5bi 243 . . . . . 6 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (¬ 𝑦 = ∅ → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
53 xpeq1 5567 . . . . . . . 8 (𝑦 = ∅ → (𝑦 × 𝐵) = (∅ × 𝐵))
5453, 15syl6eqel 2925 . . . . . . 7 (𝑦 = ∅ → (𝑦 × 𝐵) ∈ Fin)
5554a1d 25 . . . . . 6 (𝑦 = ∅ → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
5652, 55pm2.61d2 182 . . . . 5 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
5756ex 413 . . . 4 (𝑦 ∈ Fin → (𝐵 ∈ Fin → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
5857com23 86 . . 3 (𝑦 ∈ Fin → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
593, 6, 9, 12, 16, 58findcard 8749 . 2 (𝐴 ∈ Fin → (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin))
6059imp 407 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1530  wex 1773  wcel 2107  wral 3142  Vcvv 3499  cdif 3936  cun 3937  c0 4294  {csn 4563   class class class wbr 5062   × cxp 5551  cres 5555  1-1-ontowf1o 6350  2nd c2nd 7682  cen 8498  Fincfn 8501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-en 8502  df-fin 8505
This theorem is referenced by:  3xpfi  8782  mapfi  8812  fsuppxpfi  8842  infxpenlem  9431  ackbij1lem9  9642  ackbij1lem10  9643  hashxplem  13787  hashmap  13789  fsum2dlem  15117  fsumcom2  15121  ackbijnn  15175  fprod2dlem  15326  fprodcom2  15330  rexpen  15573  crth  16107  phimullem  16108  prmreclem3  16246  gsumcom3fi  19021  ablfaclem3  19131  gsumdixp  19281  gsumbagdiag  20077  psrass1lem  20078  evlslem2  20212  frlmbas3  20836  mamudm  20915  mamufacex  20916  mamures  20917  mamucl  20926  mamudi  20928  mamudir  20929  mamuvs1  20930  mamuvs2  20931  matsca2  20945  matbas2  20946  matplusg2  20952  matvsca2  20953  matplusgcell  20958  matsubgcell  20959  matvscacell  20961  matgsum  20962  mamumat1cl  20964  mattposcl  20978  mdetrsca  21128  mdetunilem9  21145  pmatcoe1fsupp  21225  tsmsxplem1  22676  tsmsxplem2  22677  tsmsxp  22678  i1fadd  24211  i1fmul  24212  itg1addlem4  24215  fsumdvdsmul  25686  fsumvma  25703  lgsquadlem1  25870  lgsquadlem2  25871  lgsquadlem3  25872  relfi  30267  fsumiunle  30459  matdim  30899  fedgmullem1  30911  sibfof  31484  hgt750lemb  31813  erdszelem10  32331  matunitlindflem2  34756  matunitlindf  34757  poimirlem26  34785  poimirlem27  34786  poimirlem28  34787  cntotbnd  34942  pellex  39293  fourierdlem42  42296  etransclem44  42425  etransclem45  42426  etransclem47  42428
  Copyright terms: Public domain W3C validator