Theorem islp2 7747

Description: The predicate "P is a limit point of S," in terms of neighborhoods. Definition of limit point in [Munkres] p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods.

Hypothesis

Ref	Expression
lpfval.1	|- X = U.J

Assertion

Ref	Expression
islp2	|- ((J e. Top /\ S (_ X /\ P e. X) -> (P e. ((limPt` J)` S) <-> A.n e. ((nei` J)` {P})(n i^i (S \ {P})) =/= (/)))

Distinct variable groups:   n,J   S,n   n,X   P,n

Proof of Theorem islp2

Step	Hyp	Ref	Expression
1		lpfval.1	. . . . 5 |- X = U.J
2	1	islp 7744	. . . 4 |- ((J e. Top /\ S (_ X) -> (P e. ((limPt` J)` S) <-> P e. ((cls` J)` (S \ {P}))))
3	1	clsval 7677	. . . . . 6 |- ((J e. Top /\ (S \ {P}) (_ X) -> ((cls` J)` (S \ {P})) = |^|{x e. (Clsd` J) | (S \ {P}) (_ x})
4		ssdifss 2168	. . . . . 6 |- (S (_ X -> (S \ {P}) (_ X)
5	3, 4	sylan2 451	. . . . 5 |- ((J e. Top /\ S (_ X) -> ((cls` J)` (S \ {P})) = |^|{x e. (Clsd` J) | (S \ {P}) (_ x})
6	5	eleq2d 1541	. . . 4 |- ((J e. Top /\ S (_ X) -> (P e. ((cls` J)` (S \ {P})) <-> P e. |^|{x e. (Clsd` J) | (S \ {P}) (_ x}))
7	2, 6	bitrd 528	. . 3 |- ((J e. Top /\ S (_ X) -> (P e. ((limPt` J)` S) <-> P e. |^|{x e. (Clsd` J) | (S \ {P}) (_ x}))
8	7	3adant3 799	. 2 |- ((J e. Top /\ S (_ X /\ P e. X) -> (P e. ((limPt` J)` S) <-> P e. |^|{x e. (Clsd` J) | (S \ {P}) (_ x}))
9		elintrabg 2546	. . . 4 |- (P e. X -> (P e. |^|{x e. (Clsd` J) | (S \ {P}) (_ x} <-> A.x e. (Clsd` J)((S \ {P}) (_ x -> P e. x)))
10	1	iscld 7669	. . . . . . 7 |- (J e. Top -> (x e. (Clsd` J) <-> (x (_ X /\ (X \ x) e. J)))
11	10	imbi1d 613	. . . . . 6 |- (J e. Top -> ((x e. (Clsd` J) -> ((S \ {P}) (_ x -> P e. x)) <-> ((x (_ X /\ (X \ x) e. J) -> ((S \ {P}) (_ x -> P e. x))))
12	11	albidv 1278	. . . . 5 |- (J e. Top -> (A.x(x e. (Clsd` J) -> ((S \ {P}) (_ x -> P e. x)) <-> A.x((x (_ X /\ (X \ x) e. J) -> ((S \ {P}) (_ x -> P e. x))))
13		df-ral 1649	. . . . 5 |- (A.x e. (Clsd` J)((S \ {P}) (_ x -> P e. x) <-> A.x(x e. (Clsd` J) -> ((S \ {P}) (_ x -> P e. x)))
14	12, 13	syl5bb 532	. . . 4 |- (J e. Top -> (A.x e. (Clsd` J)((S \ {P}) (_ x -> P e. x) <-> A.x((x (_ X /\ (X \ x) e. J) -> ((S \ {P}) (_ x -> P e. x))))
15	9, 14	sylan9bbr 541	. . 3 |- ((J e. Top /\ P e. X) -> (P e. |^|{x e. (Clsd` J) | (S \ {P}) (_ x} <-> A.x((x (_ X /\ (X \ x) e. J) -> ((S \ {P}) (_ x -> P e. x))))
16	15	3adant2 798	. 2 |- ((J e. Top /\ S (_ X /\ P e. X) -> (P e. |^|{x e. (Clsd` J) | (S \ {P}) (_ x} <-> A.x((x (_ X /\ (X \ x) e. J) -> ((S \ {P}) (_ x -> P e. x))))
17	1	isneip 7720	. . . . . . . 8 |- ((J e. Top /\ P e. X) -> (n e. ((nei` J)` {P}) <-> (n (_ X /\ E.y e. J (P e. y /\ y (_ n))))
18	17	imbi1d 613	. . . . . . 7 |- ((J e. Top /\ P e. X) -> ((n e. ((nei` J)` {P}) -> (n i^i (S \ {P})) =/= (/)) <-> ((n (_ X /\ E.y e. J (P e. y /\ y (_ n)) -> (n i^i (S \ {P})) =/= (/))))
19	18	albidv 1278	. . . . . 6 |- ((J e. Top /\ P e. X) -> (A.n(n e. ((nei` J)` {P}) -> (n i^i (S \ {P})) =/= (/)) <-> A.n((n (_ X /\ E.y e. J (P e. y /\ y (_ n)) -> (n i^i (S \ {P})) =/= (/))))
20		df-ral 1649	. . . . . 6 |- (A.n e. ((nei` J)` {P})(n i^i (S \ {P})) =/= (/) <-> A.n(n e. ((nei` J)` {P}) -> (n i^i (S \ {P})) =/= (/)))
21	19, 20	syl5bb 532	. . . . 5 |- ((J e. Top /\ P e. X) -> (A.n e. ((nei` J)` {P})(n i^i (S \ {P})) =/= (/) <-> A.n((n (_ X /\ E.y e. J (P e. y /\ y (_ n)) -> (n i^i (S \ {P})) =/= (/))))
22	21	3adant2 798	. . . 4 |- ((J e. Top /\ S (_ X /\ P e. X) -> (A.n e. ((nei` J)` {P})(n i^i (S \ {P})) =/= (/) <-> A.n((n (_ X /\ E.y e. J (P e. y /\ y (_ n)) -> (n i^i (S \ {P})) =/= (/))))
23		elpwi 2406	. . . . . . . . . . . 12 |- (n e. P~X -> n (_ X)
24		dfss4 2242	. . . . . . . . . . . 12 |- (n (_ X <-> (X \ (X \ n)) = n)
25	23, 24	sylib 198	. . . . . . . . . . 11 |- (n e. P~X -> (X \ (X \ n)) = n)
26	25	eqcomd 1480	. . . . . . . . . 10 |- (n e. P~X -> n = (X \ (X \ n)))
27	26	eleq1d 1540	. . . . . . . . 9 |- (n e. P~X -> (n e. J <-> (X \ (X \ n)) e. J))
28	27	adantl 388	. . . . . . . 8 |- (((S (_ X /\ P e. X) /\ n e. P~X) -> (n e. J <-> (X \ (X \ n)) e. J))
29		reldisj 2313	. . . . . . . . . . . . . 14 |- ((S \ {P}) (_ X -> (((S \ {P}) i^i n) = (/) <-> (S \ {P}) (_ (X \ n)))
30	4, 29	syl 10	. . . . . . . . . . . . 13 |- (S (_ X -> (((S \ {P}) i^i n) = (/) <-> (S \ {P}) (_ (X \ n)))
31		incom 2208	. . . . . . . . . . . . . 14 |- (n i^i (S \ {P})) = ((S \ {P}) i^i n)
32	31	eqeq1i 1482	. . . . . . . . . . . . 13 |- ((n i^i (S \ {P})) = (/) <-> ((S \ {P}) i^i n) = (/))
33	30, 32	syl5bb 532	. . . . . . . . . . . 12 |- (S (_ X -> ((n i^i (S \ {P})) = (/) <-> (S \ {P}) (_ (X \ n)))
34	33	adantr 389	. . . . . . . . . . 11 |- ((S (_ X /\ P e. X) -> ((n i^i (S \ {P})) = (/) <-> (S \ {P}) (_ (X \ n)))
35		eldif 2057	. . . . . . . . . . . . 13 |- (P e. (X \ n) <-> (P e. X /\ -. P e. n))
36	35	baibr 686	. . . . . . . . . . . 12 |- (P e. X -> (-. P e. n <-> P e. (X \ n)))
37	36	adantl 388	. . . . . . . . . . 11 |- ((S (_ X /\ P e. X) -> (-. P e. n <-> P e. (X \ n)))
38	34, 37	imbi12d 626	. . . . . . . . . 10 |- ((S (_ X /\ P e. X) -> (((n i^i (S \ {P})) = (/) -> -. P e. n) <-> ((S \ {P}) (_ (X \ n) -> P e. (X \ n))))
39		df-ne 1587	. . . . . . . . . . . 12 |- ((n i^i (S \ {P})) =/= (/) <-> -. (n i^i (S \ {P})) = (/))
40	39	imbi2i 185	. . . . . . . . . . 11 |- ((P e. n -> (n i^i (S \ {P})) =/= (/)) <-> (P e. n -> -. (n i^i (S \ {P})) = (/)))
41		bi2.03 165	. . . . . . . . . . 11 |- ((P e. n -> -. (n i^i (S \ {P})) = (/)) <-> ((n i^i (S \ {P})) = (/) -> -. P e. n))
42	40, 41	bitr 173	. . . . . . . . . 10 |- ((P e. n -> (n i^i (S \ {P})) =/= (/)) <-> ((n i^i (S \ {P})) = (/) -> -. P e. n))
43	38, 42	syl5bb 532	. . . . . . . . 9 |- ((S (_ X /\ P e. X) -> ((P e. n -> (n i^i (S \ {P})) =/= (/)) <-> ((S \ {P}) (_ (X \ n) -> P e. (X \ n))))
44	43	adantr 389	. . . . . . . 8 |- (((S (_ X /\ P e. X) /\ n e. P~X) -> ((P e. n -> (n i^i (S \ {P})) =/= (/)) <-> ((S \ {P}) (_ (X \ n) -> P e. (X \ n))))
45	28, 44	imbi12d 626	. . . . . . 7 |- (((S (_ X /\ P e. X)