This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 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 )