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.

Step	Hyp	Ref	Expression
1		xpeq1 5562	. . . . 5 ⊢ (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵))
2	1	eleq1d 2895	. . . 4 ⊢ (𝑥 = ∅ → ((𝑥 × 𝐵) ∈ Fin ↔ (∅ × 𝐵) ∈ Fin))
3	2	imbi2d 343	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)))
4		xpeq1 5562	. . . . 5 ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∖ {𝑧}) × 𝐵))
5	4	eleq1d 2895	. . . 4 ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → ((𝑥 × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin))
6	5	imbi2d 343	. . 3 ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin)))
7		xpeq1 5562	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵))
8	7	eleq1d 2895	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
9	8	imbi2d 343	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
10		xpeq1 5562	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵))
11	10	eleq1d 2895	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 × 𝐵) ∈ Fin ↔ (𝐴 × 𝐵) ∈ Fin))
12	11	imbi2d 343	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (𝑥 × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin)))
13		0xp 5642	. . . . 5 ⊢ (∅ × 𝐵) = ∅
14		0fin 8738	. . . . 5 ⊢ ∅ ∈ Fin
15	13, 14	eqeltri 2907	. . . 4 ⊢ (∅ × 𝐵) ∈ Fin
16	15	a1i 11	. . 3 ⊢ (𝐵 ∈ Fin → (∅ × 𝐵) ∈ Fin)
17		neq0 4307	. . . . . . 7 ⊢ (¬ 𝑦 = ∅ ↔ ∃𝑤 𝑤 ∈ 𝑦)
18		sneq 4569	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → {𝑧} = {𝑤})
19	18	difeq2d 4097	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → (𝑦 ∖ {𝑧}) = (𝑦 ∖ {𝑤}))
20	19	xpeq1d 5577	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑤 → ((𝑦 ∖ {𝑧}) × 𝐵) = ((𝑦 ∖ {𝑤}) × 𝐵))
21	20	eleq1d 2895	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin ↔ ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin))
22	21	imbi2d 343	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) ↔ (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
23	22	rspcv 3616	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → ((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin)))
24	23	adantl 484	. . . . . . . . . 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 5322	. . . . . . . . . . . . . . 15 ⊢ {𝑤} ∈ V
28		xpexg 7465	. . . . . . . . . . . . . . 15 ⊢ (({𝑤} ∈ V ∧ 𝐵 ∈ Fin) → ({𝑤} × 𝐵) ∈ V)
29	27, 28	mpan 688	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ V)
30		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Fin → 𝐵 ∈ Fin)
31		vex 3496	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
32		2ndconst 7788	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ V → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto→𝐵)
33	31, 32	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Fin → (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto→𝐵)
34		f1oen2g 8518	. . . . . . . . . . . . . 14 ⊢ ((({𝑤} × 𝐵) ∈ V ∧ 𝐵 ∈ Fin ∧ (2nd ↾ ({𝑤} × 𝐵)):({𝑤} × 𝐵)–1-1-onto→𝐵) → ({𝑤} × 𝐵) ≈ 𝐵)
35	29, 30, 33, 34	syl3anc 1366	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → ({𝑤} × 𝐵) ≈ 𝐵)
36		enfii 8727	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ ({𝑤} × 𝐵) ≈ 𝐵) → ({𝑤} × 𝐵) ∈ Fin)
37	35, 36	mpdan 685	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Fin → ({𝑤} × 𝐵) ∈ Fin)
38	37	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑤 ∈ 𝑦) → ({𝑤} × 𝐵) ∈ Fin)
39		unfi 8777	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∖ {𝑤}) × 𝐵) ∈ Fin ∧ ({𝑤} × 𝐵) ∈ Fin) → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin)
40		xpundir 5614	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵))
41		difsnid 4735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 → ((𝑦 ∖ {𝑤}) ∪ {𝑤}) = 𝑦)
42	41	xpeq1d 5577	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑦 → (((𝑦 ∖ {𝑤}) ∪ {𝑤}) × 𝐵) = (𝑦 × 𝐵))
43	40, 42	syl5eqr 2868	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑦 → (((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) = (𝑦 × 𝐵))
44	43	eleq1d 2895	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ 𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin ↔ (𝑦 × 𝐵) ∈ Fin))
45	44	biimpd 231	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 𝑦 → ((((𝑦 ∖ {𝑤}) × 𝐵) ∪ ({𝑤} × 𝐵)) ∈ Fin → (𝑦 × 𝐵) ∈ Fin))
46	45	adantl 484	. . . . . . . . . . . 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 415	. . . . . . . 8 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
51	50	exlimdv 1928	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑤 𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
52	17, 51	syl5bi 244	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (¬ 𝑦 = ∅ → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
53		xpeq1 5562	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑦 × 𝐵) = (∅ × 𝐵))
54	53, 15	syl6eqel 2919	. . . . . . 7 ⊢ (𝑦 = ∅ → (𝑦 × 𝐵) ∈ Fin)
55	54	a1d 25	. . . . . 6 ⊢ (𝑦 = ∅ → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
56	52, 55	pm2.61d2 183	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin))
57	56	ex 415	. . . 4 ⊢ (𝑦 ∈ Fin → (𝐵 ∈ Fin → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)))
58	57	com23 86	. . 3 ⊢ (𝑦 ∈ Fin → (∀𝑧 ∈ 𝑦 (𝐵 ∈ Fin → ((𝑦 ∖ {𝑧}) × 𝐵) ∈ Fin) → (𝐵 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)))
59	3, 6, 9, 12, 16, 58	findcard 8749	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin → (𝐴 × 𝐵) ∈ Fin))
60	59	imp 409	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1531  ∃wex 1774   ∈ wcel 2108  ∀wral 3136  Vcvv 3493   ∖ cdif 3931   ∪ cun 3932  ∅c0 4289  {csn 4559   class class class wbr 5057   × cxp 5546   ↾ cres 5550  –1-1-onto→wf1o 6347  2^nd c2nd 7680   ≈ cen 8498  Fincfn 8501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-en 8502  df-fin 8505

This theorem is referenced by:  3xpfi  8782  mapfi  8812  fsuppxpfi  8842  infxpenlem  9431  ackbij1lem9  9642  ackbij1lem10  9643  hashxplem  13786  hashmap  13788  fsum2dlem  15117  fsumcom2  15121  ackbijnn  15175  fprod2dlem  15326  fprodcom2  15330  rexpen  15573  crth  16107  phimullem  16108  prmreclem3  16246  gsumcom3fi  19091  ablfaclem3  19201  gsumdixp  19351  gsumbagdiag  20148  psrass1lem  20149  evlslem2  20284  frlmbas3  20912  mamudm  20991  mamufacex  20992  mamures  20993  mamucl  21002  mamudi  21004  mamudir  21005  mamuvs1  21006  mamuvs2  21007  matsca2  21021  matbas2  21022  matplusg2  21028  matvsca2  21029  matplusgcell  21034  matsubgcell  21035  matvscacell  21037  matgsum  21038  mamumat1cl  21040  mattposcl  21054  mdetrsca  21204  mdetunilem9  21221  pmatcoe1fsupp  21301  tsmsxplem1  22753  tsmsxplem2  22754  tsmsxp  22755  i1fadd  24288  i1fmul  24289  itg1addlem4  24292  fsumdvdsmul  25764  fsumvma  25781  lgsquadlem1  25948  lgsquadlem2  25949  lgsquadlem3  25950  relfi  30344  fsumiunle  30538  matdim  31006  fedgmullem1  31018  sibfof  31591  hgt750lemb  31920  erdszelem10  32440  matunitlindflem2  34881  matunitlindf  34882  poimirlem26  34910  poimirlem27  34911  poimirlem28  34912  cntotbnd  35066  pellex  39422  fourierdlem42  42424  etransclem44  42553  etransclem45  42554  etransclem47  42556