Theorem unifi 4532

Description: The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144.

Assertion

Ref	Expression
unifi	|- ((E.n e. om A ~~ n /\ A.x e. A E.n e. om x ~~ n) -> E.n e. om U.A ~~ n)

Distinct variable group:   x,n,A

Proof of Theorem unifi

Step	Hyp	Ref	Expression
1		breq2 2613	. . . 4 |- (n = m -> (A ~~ n <-> A ~~ m))
2	1	cbvrexv 1792	. . 3 |- (E.n e. om A ~~ n <-> E.m e. om A ~~ m)
3		breq2 2613	. . . . . . . . 9 |- (m = (/) -> (y ~~ m <-> y ~~ (/)))
4	3	anbi1d 615	. . . . . . . 8 |- (m = (/) -> ((y ~~ m /\ A.x e. y E.n e. om x ~~ n) <-> (y ~~ (/) /\ A.x e. y E.n e. om x ~~ n)))
5	4	imbi1d 611	. . . . . . 7 |- (m = (/) -> (((y ~~ m /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> ((y ~~ (/) /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)))
6	5	albidv 1273	. . . . . 6 |- (m = (/) -> (A.y((y ~~ m /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> A.y((y ~~ (/) /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)))
7		breq2 2613	. . . . . . . . 9 |- (m = k -> (y ~~ m <-> y ~~ k))
8	7	anbi1d 615	. . . . . . . 8 |- (m = k -> ((y ~~ m /\ A.x e. y E.n e. om x ~~ n) <-> (y ~~ k /\ A.x e. y E.n e. om x ~~ n)))
9	8	imbi1d 611	. . . . . . 7 |- (m = k -> (((y ~~ m /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> ((y ~~ k /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)))
10	9	albidv 1273	. . . . . 6 |- (m = k -> (A.y((y ~~ m /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> A.y((y ~~ k /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)))
11		breq2 2613	. . . . . . . . 9 |- (m = suc k -> (y ~~ m <-> y ~~ suc k))
12	11	anbi1d 615	. . . . . . . 8 |- (m = suc k -> ((y ~~ m /\ A.x e. y E.n e. om x ~~ n) <-> (y ~~ suc k /\ A.x e. y E.n e. om x ~~ n)))
13	12	imbi1d 611	. . . . . . 7 |- (m = suc k -> (((y ~~ m /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> ((y ~~ suc k /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)))
14	13	albidv 1273	. . . . . 6 |- (m = suc k -> (A.y((y ~~ m /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> A.y((y ~~ suc k /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)))
15		en0 4404	. . . . . . . . 9 |- (y ~~ (/) <-> y = (/))
16		unieq 2500	. . . . . . . . . . 11 |- (y = (/) -> U.y = U.(/))
17		uni0 2515	. . . . . . . . . . . 12 |- U.(/) = (/)
18		0ex 2701	. . . . . . . . . . . . 13 |- (/) e. V
19	18	enref 4372	. . . . . . . . . . . 12 |- (/) ~~ (/)
20	17, 19	eqbrtr 2624	. . . . . . . . . . 11 |- U.(/) ~~ (/)
21	16, 20	syl6eqbr 2642	. . . . . . . . . 10 |- (y = (/) -> U.y ~~ (/))
22		peano1 3139	. . . . . . . . . . 11 |- (/) e. om
23		breq2 2613	. . . . . . . . . . . 12 |- (n = (/) -> (U.y ~~ n <-> U.y ~~ (/)))
24	23	rcla4ev 1868	. . . . . . . . . . 11 |- (((/) e. om /\ U.y ~~ (/)) -> E.n e. om U.y ~~ n)
25	22, 24	mpan 693	. . . . . . . . . 10 |- (U.y ~~ (/) -> E.n e. om U.y ~~ n)
26	21, 25	syl 10	. . . . . . . . 9 |- (y = (/) -> E.n e. om U.y ~~ n)
27	15, 26	sylbi 199	. . . . . . . 8 |- (y ~~ (/) -> E.n e. om U.y ~~ n)
28	27	adantr 389	. . . . . . 7 |- ((y ~~ (/) /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)
29	28	ax-gen 960	. . . . . 6 |- A.y((y ~~ (/) /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n)
30		breq1 2612	. . . . . . . . . . 11 |- (y = z -> (y ~~ k <-> z ~~ k))
31		raleq1 1778	. . . . . . . . . . 11 |- (y = z -> (A.x e. y E.n e. om x ~~ n <-> A.x e. z E.n e. om x ~~ n))
32	30, 31	anbi12d 626	. . . . . . . . . 10 |- (y = z -> ((y ~~ k /\ A.x e. y E.n e. om x ~~ n) <-> (z ~~ k /\ A.x e. z E.n e. om x ~~ n)))
33		unieq 2500	. . . . . . . . . . . 12 |- (y = z -> U.y = U.z)
34	33	breq1d 2619	. . . . . . . . . . 11 |- (y = z -> (U.y ~~ n <-> U.z ~~ n))
35	34	rexbidv 1656	. . . . . . . . . 10 |- (y = z -> (E.n e. om U.y ~~ n <-> E.n e. om U.z ~~ n))
36	32, 35	imbi12d 624	. . . . . . . . 9 |- (y = z -> (((y ~~ k /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> ((z ~~ k /\ A.x e. z E.n e. om x ~~ n) -> E.n e. om U.z ~~ n)))
37	36	cbvalv 1309	. . . . . . . 8 |- (A.y((y ~~ k /\ A.x e. y E.n e. om x ~~ n) -> E.n e. om U.y ~~ n) <-> A.z((z ~~ k /\ A.x e. z E.n e. om x ~~ n) -> E.n e. om U.z ~~ n))
38		visset 1804	. . . . . . . . . . . . . . 15 |- k e. V
39	38	sucex 3040	. . . . . . . . . . . . . 14 |- suc k e. V
40	39	ensym 4393	. . . . . . . . . . . . 13 |- (y ~~ suc k -> suc k ~~ y)
41		visset 1804	. . . . . . . . . . . . . 14 |- y e. V
42	41	bren 4359	. . . . . . . . . . . . 13 |- (suc k ~~ y <-> E.f f:suc k-1-1-onto->y)
43	40, 42	sylib 198	. . . . . . . . . . . 12 |- (y ~~ suc k -> E.f f:suc k-1-1-onto->y)
44		unfi 4528	. . . . . . . . . . . . . . . 16 |- ((E.n e. om U.(f"k) ~~ n /\ E.n e. om (f` k) ~~ n) -> E.n e. om (U.(f"k) u. (f` k)) ~~ n)
45		visset 1804	. . . . . . . . . . . . . . . . . . . . 21 |- f e. V
46		imaexg 3400	. . . . . . . . . . . . . . . . . . . . 21 |- (f e. V -> (f"k) e. V)
47	45, 46	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (f"k) e. V
48		breq1 2612	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (f"k) -> (z ~~ k <-> (f"k) ~~ k))
49		raleq1 1778	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (f"k) -> (A.x e. z E.n e. om x ~~ n <-> A.x e. (f"k)E.n e. om x ~~ n))
50	48, 49	anbi12d 626	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (f"k) -> ((z ~~ k /\ A.x e. z E.n e. om x ~~ n) <-> ((f"k) ~~ k /\ A.x e. (f"k)E.n e. om x ~~ n)))
51		unieq 2500	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z = (f"k) -> U.z = U.(f"k))
52	51	breq1d 2619	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (f"k) -> (U.z ~~ n <-> U.(f"k) ~~ n))
53	52	rexbidv 1656	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (f"k) -> (E.n e. om U.z ~~ n <-> E.n e. om U.(f"k) ~~ n))
54	50, 53	imbi12d 624	. . . . . . . . . . . . . . . . . . . 20 |- (z = (f"k) -> (((z ~~ k /\ A.x e. z E.n e. om x ~~ n) -> E.n e. om U.z ~~ n) <-> (((f"k) ~~ k /\ A.x e. (f"k)E.n e. om x ~~ n) -> E.n e. om U.(f"k) ~~ n)))
55	47, 54	cla4v 1859	. . . . . . . . . . . . . . . . . . 19 |- (A.z((z ~~ k /\ A.x e. z E.n e. om x ~~ n) -> E.n e. om U.z ~~ n) -> (((f"k) ~~ k /\ A.x e. (f"k)E.n e. om x ~~ n) -> E.n e. om U.(f"k) ~~ n))
56	55	imp 350	. . . . . . . . . . . . . . . . . 18 |- ((A.z((z ~~ k /\ A.x e. z E.n e. om x ~~ n) -> E.n e. om U.z ~~ n) /\ ((f"k) ~~ k /\ A.x e. (f"k)E.n e. om x ~~ n)) -> E.n e. om U.(f"k) ~~ n)
57		f1of1 3673	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:suc k-1-1-onto->y -> f:suc k-1-1->y)
58		sssucid 3037	. . . . . . . . . . . . . . . . . . . . . . 23 |- k (_ suc k
59		f1ores 3688	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:suc k-1-1->y /\ k (_ suc k) -> (f |` k):k-1-1-onto->(f"k))
60	58, 59	mpan2 694	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:suc k-1-1->y -> (f |` k):k-1-1-onto->(f"k))
61	38	f1oen 4379	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f |` k):k-1-1-onto->(f"k) -> k ~~ (f"k))
62	57, 60, 61	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 |- (f:suc k-1-1-onto->y -> k ~~ (f"k))
63	47	ensym 4393	. . . . . . . . . . . . . . . . . . . . 21 |- (k ~~ (f"k) -> (f"k) ~~ k)
64	62, 63	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (f:suc k-1-1-onto->y -> (f"k) ~~ k)
65	64	adantr 389	. . . . . . . . . . . . . . . . . . 19 |- ((f:suc k-1-1-onto->y /\ A.x e. y E.n e. om x ~~ n) -> (f"k) ~~ k)
66		ssun1 2183	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f"k) (_ ((f"k) u. {(f` k)})
67	66	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:suc k-1-1-onto->y -> (