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 0fin 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