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 ∈ A B ∈ Fin → ⋃ x ∈ A B ∈ Fin

Proof

Step Hyp Ref Expression
1 raleq ⊢ w = ∅ → ∀ x ∈ w B ∈ Fin ↔ ∀ x ∈ ∅ B ∈ Fin
2 iuneq1 ⊢ w = ∅ → ⋃ x ∈ w B = ⋃ x ∈ ∅ B
3 0iun ⊢ ⋃ x ∈ ∅ B = ∅
4 2 3 eqtrdi ⊢ w = ∅ → ⋃ x ∈ w B = ∅
5 4 eleq1d ⊢ w = ∅ → ⋃ x ∈ w B ∈ Fin ↔ ∅ ∈ Fin
6 1 5 imbi12d ⊢ w = ∅ → ∀ x ∈ w B ∈ Fin → ⋃ x ∈ w B ∈ Fin ↔ ∀ x ∈ ∅ B ∈ Fin → ∅ ∈ Fin
7 raleq ⊢ w = y → ∀ x ∈ w B ∈ Fin ↔ ∀ x ∈ y B ∈ Fin
8 iuneq1 ⊢ w = y → ⋃ x ∈ w B = ⋃ x ∈ y B
9 8 eleq1d ⊢ w = y → ⋃ x ∈ w B ∈ Fin ↔ ⋃ x ∈ y B ∈ Fin
10 7 9 imbi12d ⊢ w = y → ∀ x ∈ w B ∈ Fin → ⋃ x ∈ w B ∈ Fin ↔ ∀ x ∈ y B ∈ Fin → ⋃ x ∈ y B ∈ Fin
11 raleq ⊢ w = y ∪ z → ∀ x ∈ w B ∈ Fin ↔ ∀ x ∈ y ∪ z B ∈ Fin
12 iuneq1 ⊢ w = y ∪ z → ⋃ x ∈ w B = ⋃ x ∈ y ∪ z B
13 12 eleq1d ⊢ w = y ∪ z → ⋃ x ∈ w B ∈ Fin ↔ ⋃ x ∈ y ∪ z B ∈ Fin
14 11 13 imbi12d ⊢ w = y ∪ z → ∀ x ∈ w B ∈ Fin → ⋃ x ∈ w B ∈ Fin ↔ ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ y ∪ z B ∈ Fin
15 raleq ⊢ w = A → ∀ x ∈ w B ∈ Fin ↔ ∀ x ∈ A B ∈ Fin
16 iuneq1 ⊢ w = A → ⋃ x ∈ w B = ⋃ x ∈ A B
17 16 eleq1d ⊢ w = A → ⋃ x ∈ w B ∈ Fin ↔ ⋃ x ∈ A B ∈ Fin
18 15 17 imbi12d ⊢ w = A → ∀ x ∈ w B ∈ Fin → ⋃ x ∈ w B ∈ Fin ↔ ∀ x ∈ A B ∈ Fin → ⋃ x ∈ A B ∈ Fin
19 0fi ⊢ ∅ ∈ Fin
20 19 a1i ⊢ ∀ x ∈ ∅ B ∈ Fin → ∅ ∈ Fin
21 ssun1 ⊢ y ⊆ y ∪ z
22 ssralv ⊢ y ⊆ y ∪ z → ∀ x ∈ y ∪ z B ∈ Fin → ∀ x ∈ y B ∈ Fin
23 21 22 ax-mp ⊢ ∀ x ∈ y ∪ z B ∈ Fin → ∀ x ∈ y B ∈ Fin
24 23 imim1i ⊢ ∀ x ∈ y B ∈ Fin → ⋃ x ∈ y B ∈ Fin → ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ y B ∈ Fin
25 iunxun ⊢ ⋃ x ∈ y ∪ z B = ⋃ x ∈ y B ∪ ⋃ x ∈ z B
26 nfcv ⊢ Ⅎ _ y B
27 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
28 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
29 26 27 28 cbviun ⊢ ⋃ x ∈ z B = ⋃ 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 ∈ z B = ⦋ 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 ∪ z B ∈ Fin → ⦋ z / x⦌ B ∈ Fin
42 36 41 ax-mp ⊢ ∀ x ∈ y ∪ z B ∈ Fin → ⦋ z / x⦌ B ∈ Fin
43 33 42 eqeltrid ⊢ ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ z B ∈ Fin
44 unfi ⊢ ⋃ x ∈ y B ∈ Fin ∧ ⋃ x ∈ z B ∈ Fin → ⋃ x ∈ y B ∪ ⋃ x ∈ z B ∈ Fin
45 43 44 sylan2 ⊢ ⋃ x ∈ y B ∈ Fin ∧ ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ y B ∪ ⋃ x ∈ z B ∈ Fin
46 25 45 eqeltrid ⊢ ⋃ x ∈ y B ∈ Fin ∧ ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ y ∪ z B ∈ Fin
47 46 expcom ⊢ ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ y B ∈ Fin → ⋃ x ∈ y ∪ z B ∈ Fin
48 24 47 sylcom ⊢ ∀ x ∈ y B ∈ Fin → ⋃ x ∈ y B ∈ Fin → ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ y ∪ z B ∈ Fin
49 48 a1i ⊢ y ∈ Fin → ∀ x ∈ y B ∈ Fin → ⋃ x ∈ y B ∈ Fin → ∀ x ∈ y ∪ z B ∈ Fin → ⋃ x ∈ y ∪ z B ∈ Fin
50 6 10 14 18 20 49 findcard2 ⊢ A ∈ Fin → ∀ x ∈ A B ∈ Fin → ⋃ x ∈ A B ∈ Fin
51 50 imp ⊢ A ∈ Fin ∧ ∀ x ∈ A B ∈ Fin → ⋃ x ∈ A B ∈ Fin