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 )