Theorem iunfi 9250

Description: The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 9251. Note that 𝐵 depends on 𝑥, i.e. can be thought of as 𝐵(𝑥). (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
iunfi	⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iunfi

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		raleq 3293	. . . 4 ⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ Fin))
2		iuneq1 4951	. . . . . 6 ⊢ (𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵)
3		0iun 5006	. . . . . 6 ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
4	2, 3	eqtrdi 2788	. . . . 5 ⊢ (𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∅)
5	4	eleq1d 2822	. . . 4 ⊢ (𝑤 = ∅ → (∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∅ ∈ Fin))
6	1, 5	imbi12d 344	. . 3 ⊢ (𝑤 = ∅ → ((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ Fin → ∅ ∈ Fin)))
7		raleq 3293	. . . 4 ⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ 𝑦 𝐵 ∈ Fin))
8		iuneq1 4951	. . . . 5 ⊢ (𝑤 = 𝑦 → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵)
9	8	eleq1d 2822	. . . 4 ⊢ (𝑤 = 𝑦 → (∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin))
10	7, 9	imbi12d 344	. . 3 ⊢ (𝑤 = 𝑦 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin)))
11		raleq 3293	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
12		iuneq1 4951	. . . . 5 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
13	12	eleq1d 2822	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
14	11, 13	imbi12d 344	. . 3 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)))
15		raleq 3293	. . . 4 ⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin))
16		iuneq1 4951	. . . . 5 ⊢ (𝑤 = 𝐴 → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
17	16	eleq1d 2822	. . . 4 ⊢ (𝑤 = 𝐴 → (∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin))
18	15, 17	imbi12d 344	. . 3 ⊢ (𝑤 = 𝐴 → ((∀𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin)))
19		0fi 8986	. . . 4 ⊢ ∅ ∈ Fin
20	19	a1i 11	. . 3 ⊢ (∀𝑥 ∈ ∅ 𝐵 ∈ Fin → ∅ ∈ Fin)
21		ssun1 4119	. . . . . . 7 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
22		ssralv 3991	. . . . . . 7 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∀𝑥 ∈ 𝑦 𝐵 ∈ Fin))
23	21, 22	ax-mp 5	. . . . . 6 ⊢ (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∀𝑥 ∈ 𝑦 𝐵 ∈ Fin)
24	23	imim1i 63	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin))
25		iunxun 5037	. . . . . . 7 ⊢ ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵)
26		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐵
27		nfcsb1v 3862	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
28		csbeq1a 3852	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
29	26, 27, 28	cbviun 4978	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ∪ 𝑦 ∈ {𝑧}⦋𝑦 / 𝑥⦌𝐵
30		vex 3434	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
31		csbeq1 3841	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
32	30, 31	iunxsn 5034	. . . . . . . . . 10 ⊢ ∪ 𝑦 ∈ {𝑧}⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
33	29, 32	eqtri 2760	. . . . . . . . 9 ⊢ ∪ 𝑥 ∈ {𝑧}𝐵 = ⦋𝑧 / 𝑥⦌𝐵
34		ssun2 4120	. . . . . . . . . . 11 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
35		vsnid 4608	. . . . . . . . . . 11 ⊢ 𝑧 ∈ {𝑧}
36	34, 35	sselii 3919	. . . . . . . . . 10 ⊢ 𝑧 ∈ (𝑦 ∪ {𝑧})
37		nfcsb1v 3862	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
38	37	nfel1 2916	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ∈ Fin
39		csbeq1a 3852	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
40	39	eleq1d 2822	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝐵 ∈ Fin ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ Fin))
41	38, 40	rspc 3553	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ⦋𝑧 / 𝑥⦌𝐵 ∈ Fin))
42	36, 41	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ⦋𝑧 / 𝑥⦌𝐵 ∈ Fin)
43	33, 42	eqeltrid 2841	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ {𝑧}𝐵 ∈ Fin)
44		unfi 9102	. . . . . . . 8 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∪ 𝑥 ∈ {𝑧}𝐵 ∈ Fin) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ Fin)
45	43, 44	sylan2 594	. . . . . . 7 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin) → (∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ {𝑧}𝐵) ∈ Fin)
46	25, 45	eqeltrid 2841	. . . . . 6 ⊢ ((∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin) → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)
47	46	expcom 413	. . . . 5 ⊢ (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → (∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
48	24, 47	sylcom 30	. . . 4 ⊢ ((∀𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
49	48	a1i 11	. . 3 ⊢ (𝑦 ∈ Fin → ((∀𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∪ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)))
50	6, 10, 14, 18, 20, 49	findcard2 9096	. 2 ⊢ (𝐴 ∈ Fin → (∀𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin))
51	50	imp 406	1 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ⦋csb 3838   ∪ cun 3888   ⊆ wss 3890  ∅c0 4274  {csn 4568  ∪ ciun 4934  Fincfn 8890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5374  ax-un 7686

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7815  df-en 8891  df-fin 8894

This theorem is referenced by:  unifi  9251  infssuni  9253  ixpfi  9256  ackbij1lem9  10146  ackbij1lem10  10147  fsuppmapnn0fiublem  13949  fsuppmapnn0fiub  13950  fsum2dlem  15729  fsumcom2  15733  fsumiun  15781  hashiun  15782  hash2iun  15783  ackbijnn  15790  fprod2dlem  15942  fprodcom2  15946  chnfi  18597  ablfaclem3  20061  pmatcoe1fsupp  22682  locfincmp  23507  txcmplem2  23623  alexsubALTlem3  24030  aannenlem1  26311  fsumvma  27196  numedglnl  29233  rabrexfi  32597  fsumiunle  32923  psrmonprod  33717  fedgmullem1  33795  fldextrspunlsplem  33839  poimirlem30  37993  fiphp3d  43273  hbt  43584  cnrefiisplem  46283