Theorem xpfi 9129

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.

Step	Hyp	Ref	Expression
1		xpeq1 5614	. . . . 5 ⊢ (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵))
2	1	eleq1d 2821	. . . 4 ⊢ (𝑥 = ∅ → ((𝑥 × 𝐵) ∈ Fin ↔ (∅ × 𝐵) ∈ Fin))
3	2	imbi2d 341	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)))
4		xpeq1 5614	. . . . 5 ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∖ {𝑧}) × 𝐵))
5	4	eleq1d 2821	. . . 4 ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → ((𝑥 × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin))
6	5	imbi2d 341	. . 3 ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin)))
7		xpeq1 5614	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵))
8	7	eleq1d 2821	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
9	8	imbi2d 341	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
10		xpeq1 5614	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵))
11	10	eleq1d 2821	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝐴 × 𝐵) ∈ Fin))
12	11	imbi2d 341	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin)))
13		0xp 5696	. . . . 5 ⊢ (∅ × 𝐵) = ∅
14		0fin 8992	. . . . 5 ⊢ ∅ ∈ Fin
15	13, 14	eqeltri 2833	. . . 4 ⊢ (∅ × 𝐵) ∈ Fin
16	15	a1i 11	. . 3 ⊢ (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)
17		neq0 4285	. . . . . . 7 ⊢ (¬ 𝑦 = ∅ ↔ ∃𝑤 𝑤 ∈ 𝑦)
18		sneq 4575	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → {𝑧} = {𝑤})
19	18	difeq2d 4063	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → (𝑦 ∖ {𝑧}) = (𝑦 ∖ {𝑤}))
20	19	xpeq1d 5629	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑤 → ((𝑦 ∖ {𝑧}) × 𝐵) = ((𝑦 ∖ {𝑤}) × 𝐵))
21	20	eleq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
22	21	imbi2d 341	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
23	22	rspcv 3562	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
24	23	adantl 483	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
25		pm2.27 42	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin) → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
26	25	ad2antlr 725	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin) → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
27		snex 5363	. . . . . . . . . . . . . . 15 ⊢ {𝑤} ∈ V
28		xpexg 7632	. . . . . . . . . . . . . . 15 ⊢ (({𝑤} ∈ V ∧ 𝐵 ∈ Fin) → ({𝑤} × 𝐵) ∈ V)
29	27, 28	mpan 688	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ V)
30		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Fin → 𝐵 ∈ Fin)
31		vex 3441	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
32		2ndconst 7973	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ V → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto→𝐵)
33	31, 32	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Fin → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto→𝐵)
34		f1oen2g 8789	. . . . . . . . . . . . . 14 ⊢ ((({𝑤} × 𝐵) ∈ V ∧ 𝐵 ∈ Fin ∧ (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto→𝐵) → ({𝑤} × 𝐵) ≈ 𝐵)
35	29, 30, 33, 34	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → ({𝑤} × 𝐵) ≈ 𝐵)
36		enfii 9010	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ ({𝑤} × 𝐵) ≈ 𝐵) → ({𝑤} × 𝐵) ∈ Fin)
37	35, 36	mpdan 685	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ Fin)
38	37	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → ({𝑤} × 𝐵) ∈ Fin)
39		unfi 8993	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin ∧ ({𝑤} × 𝐵) ∈ Fin) → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin)
40		xpundir 5667	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵))
41		difsnid 4749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 → ((𝑦 ∖ {𝑤}) ∪ {𝑤}) = 𝑦)
42	41	xpeq1d 5629	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑦 → (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (𝑦 × 𝐵))
43	40, 42	eqtr3id 2790	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑦 → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) = (𝑦 × 𝐵))
44	43	eleq1d 2821	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ 𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
45	44	biimpd 228	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
46	45	adantl 483	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
47	39, 46	syl5 34	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → ((((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin ∧ ({𝑤} × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
48	38, 47	mpan2d 692	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → (((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
49	24, 26, 48	3syld 60	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
50	49	ex 414	. . . . . . . 8 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
51	50	exlimdv 1934	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑤 𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
52	17, 51	biimtrid 241	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (¬ 𝑦 = ∅ → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
53		xpeq1 5614	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑦 × 𝐵) = (∅ × 𝐵))
54	53, 15	eqeltrdi 2845	. . . . . . 7 ⊢ (𝑦 = ∅ → (𝑦 × 𝐵) ∈ Fin)
55	54	a1d 25	. . . . . 6 ⊢ (𝑦 = ∅ → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
56	52, 55	pm2.61d2 181	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
57	56	ex 414	. . . 4 ⊢ (𝑦 ∈ Fin → (𝐵 ∈ Fin → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
58	57	com23 86	. . 3 ⊢ (𝑦 ∈ Fin → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
59	3, 6, 9, 12, 16, 58	findcard 8984	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin))
60	59	imp 408	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1539  ∃wex 1779   ∈ wcel 2104  ∀wral 3062  Vcvv 3437   ∖ cdif 3889   ∪ cun 3890  ∅c0 4262  {csn 4565   class class class wbr 5081   × cxp 5598   ↾ cres 5602  –1-1-onto→wf1o 6457  2^nd c2nd 7862   ≈ cen 8761  Fincfn 8764

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-om 7745  df-1st 7863  df-2nd 7864  df-1o 8328  df-en 8765  df-fin 8768

This theorem is referenced by:  3xpfi  9130  mapfi  9159  fsuppxpfi  9189  infxpenlem  9815  ficardadju  10001  ackbij1lem9  10030  ackbij1lem10  10031  hashxplem  14193  hashmap  14195  fsum2dlem  15527  fsumcom2  15531  ackbijnn  15585  fprod2dlem  15735  fprodcom2  15739  rexpen  15982  crth  16524  phimullem  16525  prmreclem3  16664  gsumcom3fi  19625  ablfaclem3  19735  gsumdixp  19893  frlmbas3  21028  gsumbagdiagOLD  21187  psrass1lemOLD  21188  gsumbagdiag  21190  psrass1lem  21191  evlslem2  21334  mamudm  21582  mamufacex  21583  mamures  21584  mamucl  21593  mamudi  21595  mamudir  21596  mamuvs1  21597  mamuvs2  21598  matsca2  21614  matbas2  21615  matplusg2  21621  matvsca2  21622  matplusgcell  21627  matsubgcell  21628  matvscacell  21630  matgsum  21631  mamumat1cl  21633  mattposcl  21647  mdetrsca  21797  mdetunilem9  21814  pmatcoe1fsupp  21895  tsmsxplem1  23349  tsmsxplem2  23350  tsmsxp  23351  i1fadd  24904  i1fmul  24905  itg1addlem4  24908  itg1addlem4OLD  24909  fsumdvdsmul  26389  fsumvma  26406  lgsquadlem1  26573  lgsquadlem2  26574  lgsquadlem3  26575  relfi  30986  fsumiunle  31188  matdim  31743  fedgmullem1  31755  sibfof  32352  hgt750lemb  32681  erdszelem10  33207  matunitlindflem2  35818  matunitlindf  35819  poimirlem26  35847  poimirlem27  35848  poimirlem28  35849  cntotbnd  35998  sticksstones22  40166  pellex  40694  mnringmulrcld  41884  fourierdlem42  43739  etransclem44  43868  etransclem45  43869  etransclem47  43871