Theorem cmsss 9275

Description: A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of [Kreyszig] p. 30.

Hypotheses

Ref	Expression
cmsss.1	|- X = dom dom D
cmsss.2	|- J = (Open` D)

Assertion

Ref	Expression
cmsss	|- ((D e. CMet /\ Y C_ X) -> ((D |` (Y X. Y)) e. CMet <-> Y e. (Clsd` J)))

Proof of Theorem cmsss

Step	Hyp	Ref	Expression
1		cmsss.1	. . . . . . . . 9 |- X = dom dom D
2		cmsss.2	. . . . . . . . 9 |- J = (Open` D)
3		visset 2295	. . . . . . . . 9 |- x e. _V
4	1, 2, 3	metelcls 9243	. . . . . . . 8 |- ((D e. Met /\ Y C_ X) -> (x e. ((cls` J)` Y) <-> E.f(f:NN-->Y /\ f(~~>m` D)x)))
5	3	lmcau 9274	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ f(~~>m` D)x) -> f e. (Cau` D))
6	5	adantrl 430	. . . . . . . . . . . . . 14 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> f e. (Cau` D))
7		causs 9233	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ f:NN-->Y) -> (f e. (Cau` D) <-> f e. (Cau` (D |` (Y X. Y)))))
8	7	adantrr 431	. . . . . . . . . . . . . 14 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (f e. (Cau` D) <-> f e. (Cau` (D |` (Y X. Y)))))
9	6, 8	mpbid 212	. . . . . . . . . . . . 13 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> f e. (Cau` (D |` (Y X. Y))))
10		eqid 1884	. . . . . . . . . . . . . . 15 |- dom dom ( D |` (Y X. Y)) = dom dom ( D |` (Y X. Y))
11	10	cmscvg 9225	. . . . . . . . . . . . . 14 |- (((D |` (Y X. Y)) e. CMet /\ f e. (Cau` (D |` (Y X. Y)))) -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y)
12	11	expcom 403	. . . . . . . . . . . . 13 |- (f e. (Cau` (D |` (Y X. Y))) -> ((D |` (Y X. Y)) e. CMet -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y))
13	9, 12	syl 12	. . . . . . . . . . . 12 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> ((D |` (Y X. Y)) e. CMet -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y))
14	13	adantlr 429	. . . . . . . . . . 11 |- (((D e. Met /\ Y C_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> ((D |` (Y X. Y)) e. CMet -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y))
15	1	metssba2 9087	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ Y C_ X) -> Y = dom dom ( D |` (Y X. Y)))
16	15	eleq2d 1964	. . . . . . . . . . . . . 14 |- ((D e. Met /\ Y C_ X) -> (y e. Y <-> y e. dom dom ( D |` (Y X. Y))))
17	16	adantr 425	. . . . . . . . . . . . 13 |- (((D e. Met /\ Y C_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. Y <-> y e. dom dom ( D |` (Y X. Y))))
18		simpll 448	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> D e. Met)
19		simplrr 455	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> f(~~>m` D)x)
20		lmss 9231	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D e. Met /\ y e. Y /\ f:NN-->Y) -> (f(~~>m` D)y <-> f(~~>m` (D |` (Y X. Y)))y))
21	20	biimprd 171	. . . . . . . . . . . . . . . . . . . . 21 |- ((D e. Met /\ y e. Y /\ f:NN-->Y) -> (f(~~>m` (D |` (Y X. Y)))y -> f(~~>m` D)y))
22	21	3exp 1066	. . . . . . . . . . . . . . . . . . . 20 |- (D e. Met -> (y e. Y -> (f:NN-->Y -> (f(~~>m` (D |` (Y X. Y)))y -> f(~~>m` D)y))))
23	22	com23 36	. . . . . . . . . . . . . . . . . . 19 |- (D e. Met -> (f:NN-->Y -> (y e. Y -> (f(~~>m` (D |` (Y X. Y)))y -> f(~~>m` D)y))))
24	23	imp43 397	. . . . . . . . . . . . . . . . . 18 |- (((D e. Met /\ f:NN-->Y) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> f(~~>m` D)y)
25	24	adantlrr 435	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> f(~~>m` D)y)
26		visset 2295	. . . . . . . . . . . . . . . . . 18 |- y e. _V
27	3, 26	lmuni 9229	. . . . . . . . . . . . . . . . 17 |- ((D e. Met /\ f(~~>m` D)x /\ f(~~>m` D)y) -> x = y)
28	18, 19, 25, 27	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> x = y)
29		eleq1a 1966	. . . . . . . . . . . . . . . . 17 |- (y e. Y -> (x = y -> x e. Y))
30	29	ad2antrl 442	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> (x = y -> x e. Y))
31	28, 30	mpd 29	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> x e. Y)
32	31	exp32 408	. . . . . . . . . . . . . 14 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. Y -> (f(~~>m` (D |` (Y X. Y)))y -> x e. Y)))
33	32	adantlr 429	. . . . . . . . . . . . 13 |- (((D e. Met /\ Y C_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. Y -> (f(~~>m` (D |` (Y X. Y)))y -> x e. Y)))
34	17, 33	sylbird 222	. . . . . . . . . . . 12 |- (((D e. Met /\ Y C_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. dom dom ( D |` (Y X. Y)) -> (f(~~>m` (D |` (Y X. Y)))y -> x e. Y)))
35	34	r19.23adv 2215	. . . . . . . . . . 11 |- (((D e. Met /\ Y C_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y -> x e. Y))
36	14, 35	syld 30	. . . . . . . . . 10 |- (((D e. Met /\ Y C_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> ((D |` (Y X. Y)) e. CMet -> x e. Y))
37	36	ex 402	. . . . . . . . 9 |- ((D e. Met /\ Y C_ X) -> ((f:NN-->Y /\ f(~~>m` D)x) -> ((D |` (Y X. Y)) e. CMet -> x e. Y)))
38	37	19.23adv 1584	. . . . . . . 8 |- ((D e. Met /\ Y C_ X) -> (E.f(f:NN-->Y /\ f(~~>m` D)x) -> ((D |` (Y X. Y)) e. CMet -> x e. Y)))
39	4, 38	sylbid 220	. . . . . . 7 |- ((D e. Met /\ Y C_ X) -> (x e. ((cls` J)` Y) -> ((D |` (Y X. Y)) e. CMet -> x e. Y)))
40	39	com23 36	. . . . . 6 |- ((D e. Met /\ Y C_ X) -> ((D |` (Y X. Y)) e. CMet -> (x e. ((cls` J)` Y) -> x e. Y)))
41	40	imp 377	. . . . 5 |- (((D e. Met /\ Y C_ X) /\ (D |` (Y X. Y)) e. CMet) -> (x e. ((cls` J)` Y) -> x e. Y))
42	41	ssrdv 2622	. . . 4 |- (((D e. Met /\ Y C_ X) /\ (D |` (Y X. Y)) e. CMet) -> ((cls` J)` Y) C_ Y)
43	2	opntop 9147	. . . . . . 7 |- (D e. Met -> J e. Top)
44	43	adantr 425	. . . . . 6 |- ((D e. Met /\ Y C_ X) -> J e. Top)
45	1, 2	uniopn2 9138	. . . . . . . 8 |- (D e. Met -> U.J = X)
46	45	sseq2d 2645	. . . . . . 7 |- (D e. Met -> (Y C_ U.J <-> Y C_ X))
47	46	biimpar 461	. . . . . 6 |- ((D e. Met /\ Y C_ X) -> Y C_ U.J)
48		eqid 1884	. . . . . . 7 |- U.J = U.J
49	48	iscld4 8972	. . . . . 6 |- ((J e. Top /\ Y C_ U.J) -> (Y e. (Clsd` J) <-> ((cls` J)` Y) C_ Y))
50	44, 47, 49	syl11anc 524	. . . . 5 |- ((D e. Met /\ Y C_ X) -> (Y e. (Clsd` J) <-> ((cls` J)` Y) C_ Y))
51	50	adantr 425	. . . 4 |- (((D e. Met /\ Y C_ X) /\ (D |` (Y X. Y)) e. CMet) -> (Y e. (Clsd` J) <-> ((cls` J)` Y) C_ Y))
52	42, 51	mpbird 213	. . 3 |- (((D e. Met /\ Y C_ X) /\ (D |` (Y X. Y)) e. CMet) -> Y e. (Clsd` J))
53		cmsmet 9239	. . 3 |- (D e. CMet -> D e. Met)
54	52, 53	sylanl1 509	. 2 |- (((D e. CMet /\ Y C_ X) /\ (D |` (Y X. Y)) e. CMet) -> Y e. (Clsd` J))
55	10	iscms2 9272	. . 3 |- ((D |` (Y X. Y)) e. CMet <-> ((D |` (Y X. Y)) e. Met /\ A.f e. (Cau` (D |` (Y X. Y)))(f:NN-->dom dom ( D |` (Y X. Y)) -> E.x e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))x)))
56		metres 9100	. . . . 5 |- (D e. Met -> (D |` (Y X. Y)) e. Met)
57	53, 56	syl 12	. . . 4 |- (D e. CMet -> (D |` (Y X. Y)) e. Met)
58	57	ad2antrr 440	. . 3 |- (((D e. CMet /\ Y C_ X) /\ Y e. (Clsd` J)) -> (D |` (Y X. Y)) e. Met)
59		caussi 9232	. . . . . . . . . . 11 |- ((D e. Met /\ f e. (Cau` (D |` (Y X. Y)))) -> f e. (Cau` D))
60	59, 53	sylan 497	. . . . . . . . . 10 |- ((D e. CMet /\ f e. (Cau` (D |` (Y X. Y)))) -> f e. (Cau` D))
61	1	cmscvg 9225	. . . . . . . . . 10 |- ((D e. CMet /\ f e. (Cau` D)) -> E.x e. X f(~~>m` D)x)
62	60, 61	syldan 516	. . . . . . . . 9 |- ((D e. CMet /\ f e. (Cau` (D |` (Y X. Y)))) -> E.x e. X f(~~>m` D)x)
63	62	ex 402	. . . . . . . 8 |- (D e. CMet -> (f e. (Cau` (D |` (Y X. Y))) -> E.x e. X f(~~>m` D)x))
64		19.8a 1376	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:NN-->Y /\ f(~~>m` D)x) -> E.f(f:NN-->Y /\ f(~~>m` D)x))
65	4, 64	syl5bir 227	. . . . . . . . . . . . . . . . . . . 20 |- ((D e. Met /\ Y C_ X) -> ((f:NN-->Y /\ f(~~>m` D)x) -> x e. ((cls` J)` Y)))
66	65	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) -> ((f:NN-->Y /\ f(~~>m` D)x) -> x e. ((cls` J)` Y)))
67		cldcls 8958	. . . . . . . . . . . . . . . . . . . . . 22 |- ((J e. Top /\ Y e. (Clsd` J)) -> ((cls` J)` Y) = Y)
68	67, 43	sylan 497	. . . . . . . . . . . . . . . . . . . . 21 |- ((D e. Met /\ Y e. (Clsd` J)) -> ((cls` J)` Y) = Y)
69	68	eleq2d 1964	. . . . . . . . . . . . . . . . . . . 20 |- ((D e. Met /\ Y e. (Clsd` J)) -> (x e. ((cls` J)` Y) <-> x e. Y))
70	69	adantlr 429	. . . . . . . . . . . . . . . . . . 19 |- (((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) -> (x e. ((cls` J)` Y) <-> x e. Y))
71	66, 70	sylibd 219	. . . . . . . . . . . . . . . . . 18 |- (((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) -> ((f:NN-->Y /\ f(~~>m` D)x) -> x e. Y))
72	71	imp 377	. . . . . . . . . . . . . . . . 17 |- ((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> x e. Y)
73	72	anassrs 489	. . . . . . . . . . . . . . . 16 |- (((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) /\ f(~~>m` D)x) -> x e. Y)
74		simpll 448	. . . . . . . . . . . . . . . . . . 19 |- (((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) -> D e. Met)
75	74	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- (((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) /\ f(~~>m` D)x) -> D e. Met)
76		simplr 449	. . . . . . . . . . . . . . . . . 18 |- (((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) /\ f(~~>m` D)x) -> f:NN-->Y)
77	75, 73, 76	3jca 1050	. . . . . . . . . . . . . . . . 17 |- (((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) /\ f(~~>m` D)x) -> (D e. Met /\ x e. Y /\ f:NN-->Y))
78		lmss 9231	. . . . . . . . . . . . . . . . . 18 |- ((D e. Met /\ x e. Y /\ f:NN-->Y) -> (f(~~>m` D)x <-> f(~~>m` (D |` (Y X. Y)))x))
79	78	biimpa 460	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ x e. Y /\ f:NN-->Y) /\ f(~~>m` D)x) -> f(~~>m` (D |` (Y X. Y)))x)
80	77, 79	sylancom 531	. . . . . . . . . . . . . . . 16 |- (((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) /\ f(~~>m` D)x) -> f(~~>m` (D |` (Y X. Y)))x)
81	73, 80	jca 310	. . . . . . . . . . . . . . 15 |- (((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) /\ f(~~>m` D)x) -> (x e. Y /\ f(~~>m` (D |` (Y X. Y)))x))
82	81	ex 402	. . . . . . . . . . . . . 14 |- ((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) -> (f(~~>m` D)x -> (x e. Y /\ f(~~>m` (D |` (Y X. Y)))x)))
83	82	adantld 426	. . . . . . . . . . . . 13 |- ((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) -> ((x e. X /\ f(~~>m` D)x) -> (x e. Y /\ f(~~>m` (D |` (Y X. Y)))x)))
84	83	reximdv2 2200	. . . . . . . . . . . 12 |- ((((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f:NN-->Y) -> (E.x e. X f(~~>m` D)x -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x))
85	84	ex 402	. . . . . . . . . . 11 |- (((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) -> (f:NN-->Y -> (E.x e. X f(~~>m` D)x -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x)))
86	85	com23 36	. . . . . . . . . 10 |- (((D e. Met /\ Y C_ X) /\ Y e. (Clsd` J)) -> (E.x e. X f(~~>m` D)x -> (f:NN-->Y -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x)))
87	86	exp31 407	. . . . . . . . 9 |- (D e. Met -> (Y C_ X -> (Y e. (Clsd` J) -> (E.x e. X f(~~>m` D)x -> (f:NN-->Y -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x)))))
88	87	com24 41	. . . . . . . 8 |- (D e. Met -> (E.x e. X f(~~>m` D)x -> (Y e. (Clsd` J) -> (Y C_ X -> (f:NN-->Y -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x)))))
89	53, 63, 88	sylsyld 32	. . . . . . 7 |- (D e. CMet -> (f e. (Cau` (D |` (Y X. Y))) -> (Y e. (Clsd` J) -> (Y C_ X -> (f:NN-->Y -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x)))))
90	89	com24 41	. . . . . 6 |- (D e. CMet -> (Y C_ X -> (Y e. (Clsd` J) -> (f e. (Cau` (D |` (Y X. Y))) -> (f:NN-->Y -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x)))))
91	90	imp41 395	. . . . 5 |- ((((D e. CMet /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f e. (Cau` (D |` (Y X. Y)))) -> (f:NN-->Y -> E.x e. Y f(~~>m` (D |` (Y X. Y)))x))
92	15, 53	sylan 497	. . . . . . 7 |- ((D e. CMet /\ Y C_ X) -> Y = dom dom ( D |` (Y X. Y)))
93		feq3 4553	. . . . . . 7 |- (Y = dom dom ( D |` (Y X. Y)) -> (f:NN-->Y <-> f:NN-->dom dom ( D |` (Y X. Y))))
94	92, 93	syl 12	. . . . . 6 |- ((D e. CMet /\ Y C_ X) -> (f:NN-->Y <-> f:NN-->dom dom ( D |` (Y X. Y))))
95	94	ad2antrr 440	. . . . 5 |- ((((D e. CMet /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f e. (Cau` (D |` (Y X. Y)))) -> (f:NN-->Y <-> f:NN-->dom dom ( D |` (Y X. Y))))
96	92	rexeqdv 2270	. . . . . 6 |- ((D e. CMet /\ Y C_ X) -> (E.x e. Y f(~~>m` (D |` (Y X. Y)))x <-> E.x e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))x))
97	96	ad2antrr 440	. . . . 5 |- ((((D e. CMet /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f e. (Cau` (D |` (Y X. Y)))) -> (E.x e. Y f(~~>m` (D |` (Y X. Y)))x <-> E.x e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))x))
98	91, 95, 97	3imtr3d 601	. . . 4 |- ((((D e. CMet /\ Y C_ X) /\ Y e. (Clsd` J)) /\ f e. (Cau` (D |` (Y X. Y)))) -> (f:NN-->dom dom ( D |` (Y X. Y)) -> E.x e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))x))
99	98	r19.21aiva 2176	. . 3 |- (((D e. CMet /\ Y C_ X) /\ Y e. (Clsd` J)) -> A.f e. (Cau` (D |` (Y X. Y)))(f:NN-->dom dom ( D |` (Y X. Y)) -> E.x e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))x))
100	55, 58, 99	sylanbrc 527	. 2 |- (((D e. CMet /\ Y C_ X) /\ Y e. (Clsd` J)) -> (D |` (Y X. Y)) e. CMet)
101	54, 100	impbida 577	1 |- ((D e. CMet /\ Y C_ X) -> ((D |` (Y X. Y)) e. CMet <-> Y e. (Clsd` J)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106   C_ wss 2593  U.cuni 3177   class class class wbr 3338   X. cxp 3984  dom cdm 3986   |` cres 3988  -->wf 3994  ` cfv 3998  NNcn 6449  Topctop 8857  Clsdccld 8936  clsccl 8938  Metcme 9066  Opencopn 9069  ~~>mclm 9197  Caucca 9198  CMetcms 9199

This theorem is referenced by:  bnsscmcl 9870  recms 16010  rrnheibor 16023

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  ax-reg 5695  ax-inf2 5731  ax-ac 5906

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-nel 2020  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-iin 3258  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-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-r1 5750  df-rank 5751  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-fl 7463  df-uz 7587  df-top 8861  df-cld 8939  df-ntr 8940  df-cls 8941  df-nei 8989  df-lp 9017  df-met 9070  df-bl 9072  df-opn 9073  df-lm 9200  df-cau 9201  df-cmet 9202

Copyright terms: Public domain