Theorem elcls 7704

Description: Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95.

Hypothesis

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

Assertion

Ref	Expression
elcls	|- ((J e. Top /\ S (_ X /\ P e. X) -> (P e. ((cls` J)` S) <-> A.x e. J (P e. x -> (x i^i S) =/= (/))))

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

Proof of Theorem elcls

Step	Hyp	Ref	Expression
1		eleq2 1535	. . . . . . 7 |- (x = (X \ ((cls` J)` S)) -> (P e. x <-> P e. (X \ ((cls` J)` S))))
2		ineq1 2210	. . . . . . . . 9 |- (x = (X \ ((cls` J)` S)) -> (x i^i S) = ((X \ ((cls` J)` S)) i^i S))
3	2	neeq1d 1594	. . . . . . . 8 |- (x = (X \ ((cls` J)` S)) -> ((x i^i S) =/= (/) <-> ((X \ ((cls` J)` S)) i^i S) =/= (/)))
4	3	negbid 611	. . . . . . 7 |- (x = (X \ ((cls` J)` S)) -> (-. (x i^i S) =/= (/) <-> -. ((X \ ((cls` J)` S)) i^i S) =/= (/)))
5	1, 4	anbi12d 628	. . . . . 6 |- (x = (X \ ((cls` J)` S)) -> ((P e. x /\ -. (x i^i S) =/= (/)) <-> (P e. (X \ ((cls` J)` S)) /\ -. ((X \ ((cls` J)` S)) i^i S) =/= (/))))
6	5	rcla4ev 1877	. . . . 5 |- (((X \ ((cls` J)` S)) e. J /\ (P e. (X \ ((cls` J)` S)) /\ -. ((X \ ((cls` J)` S)) i^i S) =/= (/))) -> E.x e. J (P e. x /\ -. (x i^i S) =/= (/)))
7		clscld.1	. . . . . . . 8 |- X = U.J
8	7	cmclsopn 7693	. . . . . . 7 |- ((J e. Top /\ S (_ X) -> (X \ ((cls` J)` S)) e. J)
9	8	3adant3 799	. . . . . 6 |- ((J e. Top /\ S (_ X /\ P e. X) -> (X \ ((cls` J)` S)) e. J)
10	9	adantr 389	. . . . 5 |- (((J e. Top /\ S (_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> (X \ ((cls` J)` S)) e. J)
11		eldif 2057	. . . . . . . 8 |- (P e. (X \ ((cls` J)` S)) <-> (P e. X /\ -. P e. ((cls` J)` S)))
12	11	biimpr 152	. . . . . . 7 |- ((P e. X /\ -. P e. ((cls` J)` S)) -> P e. (X \ ((cls` J)` S)))
13	12	3ad2antl3 811	. . . . . 6 |- (((J e. Top /\ S (_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> P e. (X \ ((cls` J)` S)))
14		pm3.27 323	. . . . . . . . . . . . 13 |- ((J e. Top /\ S (_ X) -> S (_ X)
15	7	sscls 7689	. . . . . . . . . . . . 13 |- ((J e. Top /\ S (_ X) -> S (_ ((cls` J)` S))
16	14, 15	jca 288	. . . . . . . . . . . 12 |- ((J e. Top /\ S (_ X) -> (S (_ X /\ S (_ ((cls` J)` S)))
17		ssin 2232	. . . . . . . . . . . 12 |- ((S (_ X /\ S (_ ((cls` J)` S)) <-> S (_ (X i^i ((cls` J)` S)))
18	16, 17	sylib 198	. . . . . . . . . . 11 |- ((J e. Top /\ S (_ X) -> S (_ (X i^i ((cls` J)` S)))
19		dfin4 2248	. . . . . . . . . . 11 |- (X i^i ((cls` J)` S)) = (X \ (X \ ((cls` J)` S)))
20	18, 19	syl6ss 2107	. . . . . . . . . 10 |- ((J e. Top /\ S (_ X) -> S (_ (X \ (X \ ((cls` J)` S))))
21		reldisj 2313	. . . . . . . . . . 11 |- (S (_ X -> ((S i^i (X \ ((cls` J)` S))) = (/) <-> S (_ (X \ (X \ ((cls` J)` S)))))
22	21	adantl 388	. . . . . . . . . 10 |- ((J e. Top /\ S (_ X) -> ((S i^i (X \ ((cls` J)` S))) = (/) <-> S (_ (X \ (X \ ((cls` J)` S)))))
23	20, 22	mpbird 196	. . . . . . . . 9 |- ((J e. Top /\ S (_ X) -> (S i^i (X \ ((cls` J)` S))) = (/))
24		nne 1589	. . . . . . . . . 10 |- (-. ((X \ ((cls` J)` S)) i^i S) =/= (/) <-> ((X \ ((cls` J)` S)) i^i S) = (/))
25		incom 2208	. . . . . . . . . . 11 |- ((X \ ((cls` J)` S)) i^i S) = (S i^i (X \ ((cls` J)` S)))
26	25	eqeq1i 1482	. . . . . . . . . 10 |- (((X \ ((cls` J)` S)) i^i S) = (/) <-> (S i^i (X \ ((cls` J)` S))) = (/))
27	24, 26	bitr 173	. . . . . . . . 9 |- (-. ((X \ ((cls` J)` S)) i^i S) =/= (/) <-> (S i^i (X \ ((cls` J)` S))) = (/))
28	23, 27	sylibr 200	. . . . . . . 8 |- ((J e. Top /\ S (_ X) -> -. ((X \ ((cls` J)` S)) i^i S) =/= (/))
29	28	3adant3 799	. . . . . . 7 |- ((J e. Top /\ S (_ X /\ P e. X) -> -. ((X \ ((cls` J)` S)) i^i S) =/= (/))
30	29	adantr 389	. . . . . 6 |- (((J e. Top /\ S (_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> -. ((X \ ((cls` J)` S)) i^i S) =/= (/))
31	13, 30	jca 288	. . . . 5 |- (((J e. Top /\ S (_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> (P e. (X \ ((cls` J)` S)) /\ -. ((X \ ((cls` J)` S)) i^i S) =/= (/)))
32	6, 10, 31	sylanc 471	. . . 4 |- (((J e. Top /\ S (_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> E.x e. J (P e. x /\ -. (x i^i S) =/= (/)))
33	7	clsss2 7703	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ (X \ x) e. (Clsd` J) /\ S (_ (X \ x)) -> ((cls` J)` S) (_ (X \ x))
34		pm3.26 319	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ S (_ X) -> J e. Top)
35	34	ad2antrr 404	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ (S i^i x) = (/)) -> J e. Top)
36	7	opncld 7674	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ x e. J) -> (X \ x) e. (Clsd` J))
37	36	adantlr 393	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ S (_ X) /\ x e. J) -> (X \ x) e. (Clsd` J))
38	37	adantr 389	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (X \ x) e. (Clsd` J))
39		reldisj 2313	. . . . . . . . . . . . . . . . . 18 |- (S (_ X -> ((S i^i x) = (/) <-> S (_ (X \ x)))
40	39	biimpa 416	. . . . . . . . . . . . . . . . 17 |- ((S (_ X /\ (S i^i x) = (/)) -> S (_ (X \ x))
41	40	adantll 392	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ S (_ X) /\ (S i^i x) = (/)) -> S (_ (X \ x))
42	41	adantlr 393	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ (S i^i x) = (/)) -> S (_ (X \ x))
43	33, 35, 38, 42	syl3anc 858	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ (S i^i x) = (/)) -> ((cls` J)` S) (_ (X \ x))
44	43	sseld 2067	. . . . . . . . . . . . 13 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (P e. ((cls` J)` S) -> P e. (X \ x)))
45		eldifn 2163	. . . . . . . . . . . . 13 |- (P e. (X \ x) -> -. P e. x)
46	44, 45	syl6 22	. . . . . . . . . . . 12 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (P e. ((cls` J)` S) -> -. P e. x))
47	46	con2d 91	. . . . . . . . . . 11 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (P e. x -> -. P e. ((cls` J)` S)))
48		incom 2208	. . . . . . . . . . . . 13 |- (S i^i x) = (x i^i S)
49	48	eqeq1i 1482	. . . . . . . . . . . 12 |- ((S i^i x) = (/) <-> (x i^i S) = (/))
50		df-ne 1587	. . . . . . . . . . . . 13 |- ((x i^i S) =/= (/) <-> -. (x i^i S) = (/))
51	50	con2bii 221	. . . . . . . . . . . 12 |- ((x i^i S) = (/) <-> -. (x i^i S) =/= (/))
52	49, 51	bitr 173	. . . . . . . . . . 11 |- ((S i^i x) = (/) <-> -. (x i^i S) =/= (/))
53	47, 52	sylan2br 453	. . . . . . . . . 10 |- ((((J e. Top /\ S (_ X) /\ x e. J) /\ -. (x i^i S) =/= (/)) -> (P e. x -> -. P e. ((cls` J)` S)))
54	53	exp31 376	. . . . . . . . 9 |- ((J e. Top /\ S (_ X) -> (x e. J -> (-. (x i^i S) =/= (/) -> (P e. x -> -. P e. ((cls` J)` S)))))
55	54	com34 36	. . . . . . . 8 |- ((J e. Top /\ S (_ X) -> (x e. J -> (P e. x -> (-. (x i^i S) =/= (/) -> -. P e. ((cls` J)` S)))))
56	55	imp4a 364	. . . . . . 7 <