Definition df-lp 7738

Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 7740.

Assertion

Ref	Expression
df-lp	|- limPt = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})})}

Distinct variable group:   w,v,x,y,z

Detailed syntax breakdown of Definition df-lp

Step	Hyp	Ref	Expression
1		clp 7737	. 2 class limPt
2		vz	. . . . . 6 set z
3	2	cv 957	. . . . 5 class z
4		ctop 7590	. . . . 5 class Top
5	3, 4	wcel 960	. . . 4 wff z e. Top
6		vw	. . . . . 6 set w
7	6	cv 957	. . . . 5 class w
8		vx	. . . . . . . . 9 set x
9	8	cv 957	. . . . . . . 8 class x
10	3	cuni 2507	. . . . . . . 8 class U.z
11	9, 10	wss 2050	. . . . . . 7 wff x (_ U.z
12		vy	. . . . . . . . 9 set y
13	12	cv 957	. . . . . . . 8 class y
14		vv	. . . . . . . . . . 11 set v
15	14	cv 957	. . . . . . . . . 10 class v
16	15	csn 2413	. . . . . . . . . . . 12 class {v}
17	9, 16	cdif 2047	. . . . . . . . . . 11 class (x \ {v})
18		cJ	. . . . . . . . . . . 12 class J
19		ccl 7659	. . . . . . . . . . . 12 class cls
20	18, 19	cfv 3188	. . . . . . . . . . 11 class (cls` J)
21	17, 20	cfv 3188	. . . . . . . . . 10 class ((cls` J)` (x \ {v}))
22	15, 21	wcel 960	. . . . . . . . 9 wff v e. ((cls` J)` (x \ {v}))
23	22, 14	cab 1466	. . . . . . . 8 class {v | v e. ((cls` J)` (x \ {v}))}
24	13, 23	wceq 958	. . . . . . 7 wff y = {v | v e. ((cls` J)` (x \ {v}))}
25	11, 24	wa 223	. . . . . 6 wff (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})
26	25, 8, 12	copab 2671	. . . . 5 class {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})}
27	7, 26	wceq 958	. . . 4 wff w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})}
28	5, 27	wa 223	. . 3 wff (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})})
29	28, 2, 6	copab 2671	. 2 class {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})})}
30	1, 29	wceq 958	1 wff limPt = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})})}

This definition is referenced by:  lpfval 7739

Copyright terms: Public domain