Theorem unifi 5648

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

Assertion

Ref	Expression
unifi	|- ((A e. Fin /\ A.x e. A x e. Fin) -> U.A e. Fin)

Distinct variable group:   x,A

Proof of Theorem unifi

Step	Hyp	Ref	Expression
1		isfi 5441	. . 3 |- (A e. Fin <-> E.m e. om A ~~ m)
2		breq2 3342	. . . . . . . . 9 |- (m = (/) -> (y ~~ m <-> y ~~ (/)))
3	2	anbi1d 679	. . . . . . . 8 |- (m = (/) -> ((y ~~ m /\ A.x e. y x e. Fin) <-> (y ~~ (/) /\ A.x e. y x e. Fin)))
4	3	imbi1d 675	. . . . . . 7 |- (m = (/) -> (((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> ((y ~~ (/) /\ A.x e. y x e. Fin) -> U.y e. Fin)))
5	4	albidv 1656	. . . . . 6 |- (m = (/) -> (A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> A.y((y ~~ (/) /\ A.x e. y x e. Fin) -> U.y e. Fin)))
6		breq2 3342	. . . . . . . . 9 |- (m = k -> (y ~~ m <-> y ~~ k))
7	6	anbi1d 679	. . . . . . . 8 |- (m = k -> ((y ~~ m /\ A.x e. y x e. Fin) <-> (y ~~ k /\ A.x e. y x e. Fin)))
8	7	imbi1d 675	. . . . . . 7 |- (m = k -> (((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> ((y ~~ k /\ A.x e. y x e. Fin) -> U.y e. Fin)))
9	8	albidv 1656	. . . . . 6 |- (m = k -> (A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> A.y((y ~~ k /\ A.x e. y x e. Fin) -> U.y e. Fin)))
10		breq2 3342	. . . . . . . . 9 |- (m = suc k -> (y ~~ m <-> y ~~ suc k))
11	10	anbi1d 679	. . . . . . . 8 |- (m = suc k -> ((y ~~ m /\ A.x e. y x e. Fin) <-> (y ~~ suc k /\ A.x e. y x e. Fin)))
12	11	imbi1d 675	. . . . . . 7 |- (m = suc k -> (((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> ((y ~~ suc k /\ A.x e. y x e. Fin) -> U.y e. Fin)))
13	12	albidv 1656	. . . . . 6 |- (m = suc k -> (A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> A.y((y ~~ suc k /\ A.x e. y x e. Fin) -> U.y e. Fin)))
14		en0 5482	. . . . . . . . 9 |- (y ~~ (/) <-> y = (/))
15		unieq 3185	. . . . . . . . . . 11 |- (y = (/) -> U.y = U.(/))
16		uni0 3205	. . . . . . . . . . 11 |- U.(/) = (/)
17	15, 16	syl6eq 1944	. . . . . . . . . 10 |- (y = (/) -> U.y = (/))
18		peano1 3971	. . . . . . . . . . 11 |- (/) e. om
19		ssid 2634	. . . . . . . . . . 11 |- (/) C_ (/)
20		ssnnfi 5629	. . . . . . . . . . 11 |- (((/) e. om /\ (/) C_ (/)) -> (/) e. Fin)
21	18, 19, 20	mp2an 761	. . . . . . . . . 10 |- (/) e. Fin
22	17, 21	syl6eqel 1979	. . . . . . . . 9 |- (y = (/) -> U.y e. Fin)
23	14, 22	sylbi 216	. . . . . . . 8 |- (y ~~ (/) -> U.y e. Fin)
24	23	adantr 425	. . . . . . 7 |- ((y ~~ (/) /\ A.x e. y x e. Fin) -> U.y e. Fin)
25	24	ax-gen 1305	. . . . . 6 |- A.y((y ~~ (/) /\ A.x e. y x e. Fin) -> U.y e. Fin)
26		breq1 3341	. . . . . . . . . . 11 |- (y = z -> (y ~~ k <-> z ~~ k))
27		raleq 2266	. . . . . . . . . . 11 |- (y = z -> (A.x e. y x e. Fin <-> A.x e. z x e. Fin))
28	26, 27	anbi12d 690	. . . . . . . . . 10 |- (y = z -> ((y ~~ k /\ A.x e. y x e. Fin) <-> (z ~~ k /\ A.x e. z x e. Fin)))
29		unieq 3185	. . . . . . . . . . 11 |- (y = z -> U.y = U.z)
30	29	eleq1d 1963	. . . . . . . . . 10 |- (y = z -> (U.y e. Fin <-> U.z e. Fin))
31	28, 30	imbi12d 688	. . . . . . . . 9 |- (y = z -> (((y ~~ k /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> ((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin)))
32	31	cbvalv 1696	. . . . . . . 8 |- (A.y((y ~~ k /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin))
33		visset 2295	. . . . . . . . . . . . . . 15 |- k e. _V
34	33	sucex 3892	. . . . . . . . . . . . . 14 |- suc k e. _V
35	34	ensym 5471	. . . . . . . . . . . . 13 |- (y ~~ suc k -> suc k ~~ y)
36		visset 2295	. . . . . . . . . . . . . 14 |- y e. _V
37	36	bren 5436	. . . . . . . . . . . . 13 |- (suc k ~~ y <-> E.f f:suc k-1-1-onto->y)
38	35, 37	sylib 215	. . . . . . . . . . . 12 |- (y ~~ suc k -> E.f f:suc k-1-1-onto->y)
39		visset 2295	. . . . . . . . . . . . . . . . . . . . 21 |- f e. _V
40		imaexg 4279	. . . . . . . . . . . . . . . . . . . . 21 |- (f e. _V -> (f"k) e. _V)
41	39, 40	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (f"k) e. _V
42		breq1 3341	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (f"k) -> (z ~~ k <-> (f"k) ~~ k))
43		raleq 2266	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (f"k) -> (A.x e. z x e. Fin <-> A.x e. (f"k)x e. Fin))
44	42, 43	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (f"k) -> ((z ~~ k /\ A.x e. z x e. Fin) <-> ((f"k) ~~ k /\ A.x e. (f"k)x e. Fin)))
45		unieq 3185	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (f"k) -> U.z = U.(f"k))
46	45	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (f"k) -> (U.z e. Fin <-> U.(f"k) e. Fin))
47	44, 46	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (z = (f"k) -> (((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) <-> (((f"k) ~~ k /\ A.x e. (f"k)x e. Fin) -> U.(f"k) e. Fin)))
48	41, 47	cla4v 2370	. . . . . . . . . . . . . . . . . . 19 |- (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) -> (((f"k) ~~ k /\ A.x e. (f"k)x e. Fin) -> U.(f"k) e. Fin))
49	48	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) /\ ((f"k) ~~ k /\ A.x e. (f"k)x e. Fin)) -> U.(f"k) e. Fin)
50		f1of1 4634	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:suc k-1-1-onto->y -> f:suc k-1-1->y)
51		sssucid 3742	. . . . . . . . . . . . . . . . . . . . . . 23 |- k C_ suc k
52		f1ores 4654	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:suc k-1-1->y /\ k C_ suc k) -> (f |` k):k-1-1-onto->(f"k))
53	51, 52	mpan2 760	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:suc k-1-1->y -> (f |` k):k-1-1-onto->(f"k))
54	33	f1oen 5457	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f |` k):k-1-1-onto->(f"k) -> k ~~ (f"k))
55	50, 53, 54	3syl 24	. . . . . . . . . . . . . . . . . . . . 21 |- (f:suc k-1-1-onto->y -> k ~~ (f"k))
56	41	ensym 5471	. . . . . . . . . . . . . . . . . . . . 21 |- (k ~~ (f"k) -> (f"k) ~~ k)
57	55, 56	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (f:suc k-1-1-onto->y -> (f"k) ~~ k)
58	57	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((f:suc k-1-1-onto->y /\ A.x e. y x e. Fin) -> (f"k) ~~ k)
59		ssun1 2767	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f"k) C_ ((f"k) u. {(f` k)})
60	59	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:suc k-1-1-onto->y -> (f"k) C_ ((f"k) u. {(f` k)}))
61		fnsnfv 4728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f Fn suc k /\ k e. suc k) -> {(f` k)} = (f"{k}))
62		f1ofn 4636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-1-1-onto->y -> f Fn suc k)
63	33	sucid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- k e. suc k
64	61, 62, 63	sylancl 525	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-1-1-onto->y -> {(f` k)} = (f"{k}))
65	64	uneq2d 2755	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc k-1-1-onto->y -> ((f"k) u. {(f` k)}) = ((f"k) u. (f"{k})))
66		df-suc 3663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- suc k = (k u. {k})
67	66	imaeq2i 4262	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f"suc k) = (f"(k u. {k}))
68		imaundi 4328	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f"(k u. {k})) = ((f"k) u. (f"{k}))
69	67, 68	eqtr2i 1909	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f"k) u. (f"{k})) = (f"suc k)
70	65, 69	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:suc k-1-1-onto->y -> ((f"k) u. {(f` k)}) = (f"suc k))
71		f1ofo 4643	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc k-1-1-onto->y -> f:suc k-onto->y)
72		foima 4622	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc k-onto->y -> (f"suc k) = y)
73	71, 72	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:suc k-1-1-onto->y -> (f"suc k) = y)
74	70, 73	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:suc k-1-1-onto->y -> ((f"k) u. {(f` k)}) = y)
75	60, 74	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . 21 |- (f:suc k-1-1-onto->y -> (f"k) C_ y)
76		ssralv 2672	. . . . . . . . . . . . . . . . . . . . 21 |- ((f"k) C_ y -> (A.x e. y x e. Fin -> A.x e. (f"k)x e. Fin))
77	75, 76	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (f:suc k-1-1-onto->y -> (A.x e. y x e. Fin -> A.x e. (f"k)x e. Fin))
78	77	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((f:suc k-1-1-onto->y /\ A.x e. y x e. Fin) -> A.x e. (f"k)x e. Fin)
79	58, 78	jca 310	. . . . . . . . . . . . . . . . . 18 |- ((f:suc k-1-1-onto->y /\ A.x e. y x e. Fin) -> ((f"k) ~~ k /\ A.x e. (f"k)x e. Fin))
80	49, 79	sylan2 500	. . . . . . . . . . . . . . . . 17 |- ((A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) /\ (f:suc k-1-1-onto->y /\ A.x e. y x e. Fin)) -> U.(f"k) e. Fin)
81	80	an1s 544	. . . . . . . . . . . . . . . 16 |- ((f:suc k-1-1-onto->y /\ (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) /\ A.x e. y x e. Fin)) -> U.(f"k) e. Fin)
82		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (x = (f` k) -> (x e. Fin <-> (f` k) e. Fin))
83	82	rcla4va 2378	. . . . . . . . . . . . . . . . . 18 |- (((f` k) e. y /\ A.x e. y x e. Fin) -> (f` k) e. Fin)
84		ffvelrn 4787	. . . . . . . . . . . . . . . . . . 19 |- ((f:suc k-->y /\ k e. suc k) -> (f` k) e. y)
85		f1of 4635	. . . . . . . . . . . . . . . . . . 19 |- (f:suc k-1-1-onto->y -> f:suc k-->y)
86	84, 85, 63	sylancl 525	. . . . . . . . . . . . . . . . . 18 |- (f:suc k-1-1-onto->y -> (f` k) e. y)
87	83, 86	sylan 497	. . . . . . . . . . . . . . . . 17 |- ((f:suc k-1-1-onto->y /\ A.x e. y x e. Fin) -> (f` k) e. Fin)
88	87	adantrl 430	. . . . . . . . . . . . . . . 16 |- ((f:suc k-1-1-onto->y /\ (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) /\ A.x e. y x e. Fin)) -> (f` k) e. Fin)
89		unfi 5644	. . . . . . . . . . . . . . . 16 |- ((U.(f"k) e. Fin /\ (f` k) e. Fin) -> (U.(f"k) u. (f` k)) e. Fin)
90	81, 88, 89	syl11anc 524	. . . . . . . . . . . . . . 15 |- ((f:suc k-1-1-onto->y /\ (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) /\ A.x e. y x e. Fin)) -> (U.(f"k) u. (f` k)) e. Fin)
91	74	unieqd 3188	. . . . . . . . . . . . . . . . . 18 |- (f:suc k-1-1-onto->y -> U.((f"k) u. {(f` k)}) = U.y)
92		uniun 3196	. . . . . . . . . . . . . . . . . . 19 |- U.((f"k) u. {(f` k)}) = (U.(f"k) u. U.{(f` k)})
93		fvex 4689	. . . . . . . . . . . . . . . . . . . . 21 |- (f` k) e. _V
94	93	unisn 3193	. . . . . . . . . . . . . . . . . . . 20 |- U.{(f` k)} = (f` k)
95	94	uneq2i 2752	. . . . . . . . . . . . . . . . . . 19 |- (U.(f"k) u. U.{(f` k)}) = (U.(f"k) u. (f` k))
96	92, 95	eqtr2i 1909	. . . . . . . . . . . . . . . . . 18 |- (U.(f"k) u. (f` k)) = U.((f"k) u. {(f` k)})
97	91, 96	syl5eq 1940	. . . . . . . . . . . . . . . . 17 |- (f:suc k-1-1-onto->y -> (U.(f"k) u. (f` k)) = U.y)
98	97	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (f:suc k-1-1-onto->y -> ((U.(f"k) u. (f` k)) e. Fin <-> U.y e. Fin))
99	98	adantr 425	. . . . . . . . . . . . . . 15 |- ((f:suc k-1-1-onto->y /\ (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) /\ A.x e. y x e. Fin)) -> ((U.(f"k) u. (f` k)) e. Fin <-> U.y e. Fin))
100	90, 99	mpbid 212	. . . . . . . . . . . . . 14 |- ((f:suc k-1-1-onto->y /\ (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) /\ A.x e. y x e. Fin)) -> U.y e. Fin)
101	100	exp32 408	. . . . . . . . . . . . 13 |- (f:suc k-1-1-onto->y -> (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) -> (A.x e. y x e. Fin -> U.y e. Fin)))
102	101	19.23aiv 1674	. . . . . . . . . . . 12 |- (E.f f:suc k-1-1-onto->y -> (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) -> (A.x e. y x e. Fin -> U.y e. Fin)))
103	38, 102	syl 12	. . . . . . . . . . 11 |- (y ~~ suc k -> (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) -> (A.x e. y x e. Fin -> U.y e. Fin)))
104	103	com12 14	. . . . . . . . . 10 |- (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) -> (y ~~ suc k -> (A.x e. y x e. Fin -> U.y e. Fin)))
105	104	imp3a 388	. . . . . . . . 9 |- (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) -> ((y ~~ suc k /\ A.x e. y x e. Fin) -> U.y e. Fin))
106	105	19.21aiv 1664	. . . . . . . 8 |- (A.z((z ~~ k /\ A.x e. z x e. Fin) -> U.z e. Fin) -> A.y((y ~~ suc k /\ A.x e. y x e. Fin) -> U.y e. Fin))
107	32, 106	sylbi 216	. . . . . . 7 |- (A.y((y ~~ k /\ A.x e. y x e. Fin) -> U.y e. Fin) -> A.y((y ~~ suc k /\ A.x e. y x e. Fin) -> U.y e. Fin))
108	107	a1i 8	. . . . . 6 |- (k e. om -> (A.y((y ~~ k /\ A.x e. y x e. Fin) -> U.y e. Fin) -> A.y((y ~~ suc k /\ A.x e. y x e. Fin) -> U.y e. Fin)))
109	5, 9, 13, 25, 108	finds1 3982	. . . . 5 |- (m e. om -> A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin))
110		relen 5431	. . . . . . . 8 |- Rel ~~
111	110	brrelexi 4029	. . . . . . 7 |- (A ~~ m -> A e. _V)
112		breq1 3341	. . . . . . . . . . 11 |- (y = A -> (y ~~ m <-> A ~~ m))
113		raleq 2266	. . . . . . . . . . 11 |- (y = A -> (A.x e. y x e. Fin <-> A.x e. A x e. Fin))
114	112, 113	anbi12d 690	. . . . . . . . . 10 |- (y = A -> ((y ~~ m /\ A.x e. y x e. Fin) <-> (A ~~ m /\ A.x e. A x e. Fin)))
115		unieq 3185	. . . . . . . . . . 11 |- (y = A -> U.y = U.A)
116	115	eleq1d 1963	. . . . . . . . . 10 |- (y = A -> (U.y e. Fin <-> U.A e. Fin))
117	114, 116	imbi12d 688	. . . . . . . . 9 |- (y = A -> (((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) <-> ((A ~~ m /\ A.x e. A x e. Fin) -> U.A e. Fin)))
118	117	cla4gv 2364	. . . . . . . 8 |- (A e. _V -> (A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) -> ((A ~~ m /\ A.x e. A x e. Fin) -> U.A e. Fin)))
119	118	exp4a 409	. . . . . . 7 |- (A e. _V -> (A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) -> (A ~~ m -> (A.x e. A x e. Fin -> U.A e. Fin))))
120	111, 119	syl 12	. . . . . 6 |- (A ~~ m -> (A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) -> (A ~~ m -> (A.x e. A x e. Fin -> U.A e. Fin))))
121	120	pm2.43b 81	. . . . 5 |- (A.y((y ~~ m /\ A.x e. y x e. Fin) -> U.y e. Fin) -> (A ~~ m -> (A.x e. A x e. Fin -> U.A e. Fin)))
122	109, 121	syl 12	. . . 4 |- (m e. om -> (A ~~ m -> (A.x e. A x e. Fin -> U.A e. Fin)))
123	122	r19.23aiv 2211	. . 3 |- (E.m e. om A ~~ m -> (A.x e. A x e. Fin -> U.A e. Fin))
124	1, 123	sylbi 216	. 2 |- (A e. Fin -> (A.x e. A x e. Fin -> U.A e. Fin))
125	124	imp 377	1 |- ((A e. Fin /\ A.x e. A x e. Fin) -> U.A e. Fin)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177   class class class wbr 3338  suc csuc 3659  omcom 3949   |` cres 3988  "cima 3989   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   ~~ cen 5423  Fincfn 5426

This theorem is referenced by:  unifi2 5649  iunfi 5659  heiborlem23 15977

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430

Copyright terms: Public domain