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

Theorem xpfi 8116
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 5052 . . . . 5 (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵))
21eleq1d 2672 . . . 4 (𝑥 = ∅ → ((𝑥 × 𝐵) ∈ Fin ↔ (∅ × 𝐵) ∈ Fin))
32imbi2d 329 . . 3 (𝑥 = ∅ → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)))
4 xpeq1 5052 . . . . 5 (𝑥 = (𝑦 ∖ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∖ {𝑧}) × 𝐵))
54eleq1d 2672 . . . 4 (𝑥 = (𝑦 ∖ {𝑧}) → ((𝑥 × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin))
65imbi2d 329 . . 3 (𝑥 = (𝑦 ∖ {𝑧}) → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin)))
7 xpeq1 5052 . . . . 5 (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵))
87eleq1d 2672 . . . 4 (𝑥 = 𝑦 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
98imbi2d 329 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
10 xpeq1 5052 . . . . 5 (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵))
1110eleq1d 2672 . . . 4 (𝑥 = 𝐴 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝐴 × 𝐵) ∈ Fin))
1211imbi2d 329 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin)))
13 0xp 5122 . . . . 5 (∅ × 𝐵) = ∅
14 0fin 8073 . . . . 5 ∅ ∈ Fin
1513, 14eqeltri 2684 . . . 4 (∅ × 𝐵) ∈ Fin
1615a1i 11 . . 3 (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)
17 neq0 3889 . . . . . . 7 𝑦 = ∅ ↔ ∃𝑤 𝑤𝑦)
18 sneq 4135 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → {𝑧} = {𝑤})
1918difeq2d 3690 . . . . . . . . . . . . . . 15 (𝑧 = 𝑤 → (𝑦 ∖ {𝑧}) = (𝑦 ∖ {𝑤}))
2019xpeq1d 5062 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → ((𝑦 ∖ {𝑧}) × 𝐵) = ((𝑦 ∖ {𝑤}) × 𝐵))
2120eleq1d 2672 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
2221imbi2d 329 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
2322rspcv 3278 . . . . . . . . . . 11 (𝑤𝑦 → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
2423adantl 481 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
25 pm2.27 41 . . . . . . . . . . 11 (𝐵 ∈ Fin → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin) → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
2625ad2antlr 759 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin) → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
27 snex 4835 . . . . . . . . . . . . . . 15 {𝑤} ∈ V
28 xpexg 6858 . . . . . . . . . . . . . . 15 (({𝑤} ∈ V ∧ 𝐵 ∈ Fin) → ({𝑤} × 𝐵) ∈ V)
2927, 28mpan 702 . . . . . . . . . . . . . 14 (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ V)
30 id 22 . . . . . . . . . . . . . 14 (𝐵 ∈ Fin → 𝐵 ∈ Fin)
31 vex 3176 . . . . . . . . . . . . . . 15 𝑤 ∈ V
32 2ndconst 7153 . . . . . . . . . . . . . . 15 (𝑤 ∈ V → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto𝐵)
3331, 32mp1i 13 . . . . . . . . . . . . . 14 (𝐵 ∈ Fin → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto𝐵)
34 f1oen2g 7858 . . . . . . . . . . . . . 14 ((({𝑤} × 𝐵) ∈ V ∧ 𝐵 ∈ Fin ∧ (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto𝐵) → ({𝑤} × 𝐵) ≈ 𝐵)
3529, 30, 33, 34syl3anc 1318 . . . . . . . . . . . . 13 (𝐵 ∈ Fin → ({𝑤} × 𝐵) ≈ 𝐵)
36 enfii 8062 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ ({𝑤} × 𝐵) ≈ 𝐵) → ({𝑤} × 𝐵) ∈ Fin)
3735, 36mpdan 699 . . . . . . . . . . . 12 (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ Fin)
3837ad2antlr 759 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ({𝑤} × 𝐵) ∈ Fin)
39 unfi 8112 . . . . . . . . . . . 12 ((((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin ∧ ({𝑤} × 𝐵) ∈ Fin) → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin)
40 xpundir 5095 . . . . . . . . . . . . . . . 16 (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵))
41 difsnid 4282 . . . . . . . . . . . . . . . . 17 (𝑤𝑦 → ((𝑦 ∖ {𝑤}) ∪ {𝑤}) = 𝑦)
4241xpeq1d 5062 . . . . . . . . . . . . . . . 16 (𝑤𝑦 → (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (𝑦 × 𝐵))
4340, 42syl5eqr 2658 . . . . . . . . . . . . . . 15 (𝑤𝑦 → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) = (𝑦 × 𝐵))
4443eleq1d 2672 . . . . . . . . . . . . . 14 (𝑤𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
4544biimpd 218 . . . . . . . . . . . . 13 (𝑤𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
4645adantl 481 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
4739, 46syl5 33 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → ((((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin ∧ ({𝑤} × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
4838, 47mpan2d 706 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → (((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
4924, 26, 483syld 58 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤𝑦) → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
5049ex 449 . . . . . . . 8 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑤𝑦 → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
5150exlimdv 1848 . . . . . . 7 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑤 𝑤𝑦 → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
5217, 51syl5bi 231 . . . . . 6 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (¬ 𝑦 = ∅ → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
53 xpeq1 5052 . . . . . . . 8 (𝑦 = ∅ → (𝑦 × 𝐵) = (∅ × 𝐵))
5453, 15syl6eqel 2696 . . . . . . 7 (𝑦 = ∅ → (𝑦 × 𝐵) ∈ Fin)
5554a1d 25 . . . . . 6 (𝑦 = ∅ → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
5652, 55pm2.61d2 171 . . . . 5 ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
5756ex 449 . . . 4 (𝑦 ∈ Fin → (𝐵 ∈ Fin → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
5857com23 84 . . 3 (𝑦 ∈ Fin → (∀𝑧𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
593, 6, 9, 12, 16, 58findcard 8084 . 2 (𝐴 ∈ Fin → (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin))
6059imp 444 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1475  wex 1695  wcel 1977  wral 2896  Vcvv 3173  cdif 3537  cun 3538  c0 3874  {csn 4125   class class class wbr 4583   × cxp 5036  cres 5040  1-1-ontowf1o 5803  2nd c2nd 7058  cen 7838  Fincfn 7841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845
This theorem is referenced by:  3xpfi  8117  mapfi  8145  fsuppxpfi  8175  infxpenlem  8719  ackbij1lem9  8933  ackbij1lem10  8934  hashxplem  13080  hashmap  13082  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  ackbijnn  14399  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  rexpen  14796  crth  15321  phimullem  15322  prmreclem3  15460  ablfaclem3  18309  gsumdixp  18432  gsumbagdiag  19197  psrass1lem  19198  evlslem2  19333  frlmbas3  19934  mamudm  20013  mamufacex  20014  mamures  20015  gsumcom3fi  20025  mamucl  20026  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  matsca2  20045  matbas2  20046  matplusg2  20052  matvsca2  20053  matplusgcell  20058  matsubgcell  20059  matvscacell  20061  matgsum  20062  mamumat1cl  20064  mattposcl  20078  mdetrsca  20228  mdetunilem9  20245  pmatcoe1fsupp  20325  tsmsxplem1  21766  tsmsxplem2  21767  tsmsxp  21768  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  fsumdvdsmul  24721  fsumvma  24738  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  relfi  28797  sibfof  29729  erdszelem10  30436  matunitlindflem2  32576  matunitlindf  32577  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  cntotbnd  32765  pellex  36417  fourierdlem42  39042  etransclem44  39171  etransclem45  39172  etransclem47  39174
  Copyright terms: Public domain W3C validator