Theorem iunfi

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

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

Proof

Step	Hyp	Ref	Expression
1		raleq	⊢ ( 𝑤 = ∅ → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀ 𝑥 ∈ ∅ 𝐵 ∈ Fin ) )
2		iuneq1	⊢ ( 𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 )
3		0iun	⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
4	2 3	eqtrdi	⊢ ( 𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∅ )
5	4	eleq1d	⊢ ( 𝑤 = ∅ → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∅ ∈ Fin ) )
6	1 5	imbi12d	⊢ ( 𝑤 = ∅ → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ) ↔ ( ∀ 𝑥 ∈ ∅ 𝐵 ∈ Fin → ∅ ∈ Fin ) ) )
7		raleq	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) )
8		iuneq1	⊢ ( 𝑤 = 𝑦 → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ 𝑦 𝐵 )
9	8	eleq1d	⊢ ( 𝑤 = 𝑦 → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) )
10	7 9	imbi12d	⊢ ( 𝑤 = 𝑦 → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ) ↔ ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) ) )
11		raleq	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) )
12		iuneq1	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
13	12	eleq1d	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) )
14	11 13	imbi12d	⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ) ↔ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) ) )
15		raleq	⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) )
16		iuneq1	⊢ ( 𝑤 = 𝐴 → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 )
17	16	eleq1d	⊢ ( 𝑤 = 𝐴 → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ↔ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) )
18	15 17	imbi12d	⊢ ( 𝑤 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑤 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ Fin ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) ) )
19		0fi	⊢ ∅ ∈ Fin
20	19	a1i	⊢ ( ∀ 𝑥 ∈ ∅ 𝐵 ∈ Fin → ∅ ∈ Fin )
21		ssun1	⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
22		ssralv	⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ∀ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) )
23	21 22	ax-mp	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ∀ 𝑥 ∈ 𝑦 𝐵 ∈ Fin )
24	23	imim1i	⊢ ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) )
25		iunxun	⊢ ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 )
26		nfcv	⊢ Ⅎ 𝑦 𝐵
27		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
28		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
29	26 27 28	cbviun	⊢ ∪ 𝑥 ∈ { 𝑧 } 𝐵 = ∪ 𝑦 ∈ { 𝑧 } ⦋ 𝑦 / 𝑥 ⦌ 𝐵
30		vex	⊢ 𝑧 ∈ V
31		csbeq1	⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
32	30 31	iunxsn	⊢ ∪ 𝑦 ∈ { 𝑧 } ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵
33	29 32	eqtri	⊢ ∪ 𝑥 ∈ { 𝑧 } 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵
34		ssun2	⊢ { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } )
35		vsnid	⊢ 𝑧 ∈ { 𝑧 }
36	34 35	sselii	⊢ 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } )
37		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
38	37	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ Fin
39		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
40	39	eleq1d	⊢ ( 𝑥 = 𝑧 → ( 𝐵 ∈ Fin ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ Fin ) )
41	38 40	rspc	⊢ ( 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ Fin ) )
42	36 41	ax-mp	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ Fin )
43	33 42	eqeltrid	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ∪ 𝑥 ∈ { 𝑧 } 𝐵 ∈ Fin )
44		unfi	⊢ ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ∈ Fin ) → ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ) ∈ Fin )
45	43 44	sylan2	⊢ ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) → ( ∪ 𝑥 ∈ 𝑦 𝐵 ∪ ∪ 𝑥 ∈ { 𝑧 } 𝐵 ) ∈ Fin )
46	25 45	eqeltrid	⊢ ( ( ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) → ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin )
47	46	expcom	⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ( ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) )
48	24 47	sylcom	⊢ ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) )
49	48	a1i	⊢ ( 𝑦 ∈ Fin → ( ( ∀ 𝑥 ∈ 𝑦 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ Fin ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin → ∪ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ∈ Fin ) ) )
50	6 10 14 18 20 49	findcard2	⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) )
51	50	imp	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin )