Metamath Proof Explorer

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 ⊢A∈Fin∧∀x∈AB∈Fin→⋃x∈AB∈Fin

Proof

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