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 e. Fin /\ A. x e. A B e. Fin ) -> U_ x e. A B e. Fin )

Proof

Step Hyp Ref Expression
1 raleq 
 |-  ( w = (/) -> ( A. x e. w B e. Fin <-> A. x e. (/) B e. Fin ) )
2 iuneq1 
 |-  ( w = (/) -> U_ x e. w B = U_ x e. (/) B )
3 0iun 
 |-  U_ x e. (/) B = (/)
4 2 3 eqtrdi 
 |-  ( w = (/) -> U_ x e. w B = (/) )
5 4 eleq1d 
 |-  ( w = (/) -> ( U_ x e. w B e. Fin <-> (/) e. Fin ) )
6 1 5 imbi12d 
 |-  ( w = (/) -> ( ( A. x e. w B e. Fin -> U_ x e. w B e. Fin ) <-> ( A. x e. (/) B e. Fin -> (/) e. Fin ) ) )
7 raleq 
 |-  ( w = y -> ( A. x e. w B e. Fin <-> A. x e. y B e. Fin ) )
8 iuneq1 
 |-  ( w = y -> U_ x e. w B = U_ x e. y B )
9 8 eleq1d 
 |-  ( w = y -> ( U_ x e. w B e. Fin <-> U_ x e. y B e. Fin ) )
10 7 9 imbi12d 
 |-  ( w = y -> ( ( A. x e. w B e. Fin -> U_ x e. w B e. Fin ) <-> ( A. x e. y B e. Fin -> U_ x e. y B e. Fin ) ) )
11 raleq 
 |-  ( w = ( y u. { z } ) -> ( A. x e. w B e. Fin <-> A. x e. ( y u. { z } ) B e. Fin ) )
12 iuneq1 
 |-  ( w = ( y u. { z } ) -> U_ x e. w B = U_ x e. ( y u. { z } ) B )
13 12 eleq1d 
 |-  ( w = ( y u. { z } ) -> ( U_ x e. w B e. Fin <-> U_ x e. ( y u. { z } ) B e. Fin ) )
14 11 13 imbi12d 
 |-  ( w = ( y u. { z } ) -> ( ( A. x e. w B e. Fin -> U_ x e. w B e. Fin ) <-> ( A. x e. ( y u. { z } ) B e. Fin -> U_ x e. ( y u. { z } ) B e. Fin ) ) )
15 raleq 
 |-  ( w = A -> ( A. x e. w B e. Fin <-> A. x e. A B e. Fin ) )
16 iuneq1 
 |-  ( w = A -> U_ x e. w B = U_ x e. A B )
17 16 eleq1d 
 |-  ( w = A -> ( U_ x e. w B e. Fin <-> U_ x e. A B e. Fin ) )
18 15 17 imbi12d 
 |-  ( w = A -> ( ( A. x e. w B e. Fin -> U_ x e. w B e. Fin ) <-> ( A. x e. A B e. Fin -> U_ x e. A B e. Fin ) ) )
19 0fin 
 |-  (/) e. Fin
20 19 a1i 
 |-  ( A. x e. (/) B e. Fin -> (/) e. Fin )
21 ssun1 
 |-  y C_ ( y u. { z } )
22 ssralv 
 |-  ( y C_ ( y u. { z } ) -> ( A. x e. ( y u. { z } ) B e. Fin -> A. x e. y B e. Fin ) )
23 21 22 ax-mp 
 |-  ( A. x e. ( y u. { z } ) B e. Fin -> A. x e. y B e. Fin )
24 23 imim1i 
 |-  ( ( A. x e. y B e. Fin -> U_ x e. y B e. Fin ) -> ( A. x e. ( y u. { z } ) B e. Fin -> U_ x e. y B e. Fin ) )
25 iunxun 
 |-  U_ x e. ( y u. { z } ) B = ( U_ x e. y B u. U_ x e. { z } B )
26 nfcv 
 |-  F/_ y B
27 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
28 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
29 26 27 28 cbviun 
 |-  U_ x e. { z } B = U_ y e. { z } [_ y / x ]_ B
30 vex 
 |-  z e. _V
31 csbeq1 
 |-  ( y = z -> [_ y / x ]_ B = [_ z / x ]_ B )
32 30 31 iunxsn 
 |-  U_ y e. { z } [_ y / x ]_ B = [_ z / x ]_ B
33 29 32 eqtri 
 |-  U_ x e. { z } B = [_ z / x ]_ B
34 ssun2 
 |-  { z } C_ ( y u. { z } )
35 vsnid 
 |-  z e. { z }
36 34 35 sselii 
 |-  z e. ( y u. { z } )
37 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
38 37 nfel1 
 |-  F/ x [_ z / x ]_ B e. Fin
39 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
40 39 eleq1d 
 |-  ( x = z -> ( B e. Fin <-> [_ z / x ]_ B e. Fin ) )
41 38 40 rspc 
 |-  ( z e. ( y u. { z } ) -> ( A. x e. ( y u. { z } ) B e. Fin -> [_ z / x ]_ B e. Fin ) )
42 36 41 ax-mp 
 |-  ( A. x e. ( y u. { z } ) B e. Fin -> [_ z / x ]_ B e. Fin )
43 33 42 eqeltrid 
 |-  ( A. x e. ( y u. { z } ) B e. Fin -> U_ x e. { z } B e. Fin )
44 unfi 
 |-  ( ( U_ x e. y B e. Fin /\ U_ x e. { z } B e. Fin ) -> ( U_ x e. y B u. U_ x e. { z } B ) e. Fin )
45 43 44 sylan2 
 |-  ( ( U_ x e. y B e. Fin /\ A. x e. ( y u. { z } ) B e. Fin ) -> ( U_ x e. y B u. U_ x e. { z } B ) e. Fin )
46 25 45 eqeltrid 
 |-  ( ( U_ x e. y B e. Fin /\ A. x e. ( y u. { z } ) B e. Fin ) -> U_ x e. ( y u. { z } ) B e. Fin )
47 46 expcom 
 |-  ( A. x e. ( y u. { z } ) B e. Fin -> ( U_ x e. y B e. Fin -> U_ x e. ( y u. { z } ) B e. Fin ) )
48 24 47 sylcom 
 |-  ( ( A. x e. y B e. Fin -> U_ x e. y B e. Fin ) -> ( A. x e. ( y u. { z } ) B e. Fin -> U_ x e. ( y u. { z } ) B e. Fin ) )
49 48 a1i 
 |-  ( y e. Fin -> ( ( A. x e. y B e. Fin -> U_ x e. y B e. Fin ) -> ( A. x e. ( y u. { z } ) B e. Fin -> U_ x e. ( y u. { z } ) B e. Fin ) ) )
50 6 10 14 18 20 49 findcard2 
 |-  ( A e. Fin -> ( A. x e. A B e. Fin -> U_ x e. A B e. Fin ) )
51 50 imp 
 |-  ( ( A e. Fin /\ A. x e. A B e. Fin ) -> U_ x e. A B e. Fin )