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 0fin ∅ ∈ 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 )