Theorem elcls 8980

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 C_ 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		clscld.1	. . . . . . . 8 |- X = U.J
2	1	cmclsopn 8969	. . . . . . 7 |- ((J e. Top /\ S C_ X) -> (X \ ((cls` J)` S)) e. J)
3	2	3adant3 896	. . . . . 6 |- ((J e. Top /\ S C_ X /\ P e. X) -> (X \ ((cls` J)` S)) e. J)
4	3	adantr 425	. . . . 5 |- (((J e. Top /\ S C_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> (X \ ((cls` J)` S)) e. J)
5		eldif 2609	. . . . . . 7 |- (P e. (X \ ((cls` J)` S)) <-> (P e. X /\ -. P e. ((cls` J)` S)))
6	5	biimpri 169	. . . . . 6 |- ((P e. X /\ -. P e. ((cls` J)` S)) -> P e. (X \ ((cls` J)` S)))
7	6	3ad2antl3 1040	. . . . 5 |- (((J e. Top /\ S C_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> P e. (X \ ((cls` J)` S)))
8		simpr 350	. . . . . . . . . . . 12 |- ((J e. Top /\ S C_ X) -> S C_ X)
9	1	sscls 8965	. . . . . . . . . . . 12 |- ((J e. Top /\ S C_ X) -> S C_ ((cls` J)` S))
10	8, 9	jca 310	. . . . . . . . . . 11 |- ((J e. Top /\ S C_ X) -> (S C_ X /\ S C_ ((cls` J)` S)))
11		ssin 2814	. . . . . . . . . . 11 |- ((S C_ X /\ S C_ ((cls` J)` S)) <-> S C_ (X i^i ((cls` J)` S)))
12	10, 11	sylib 215	. . . . . . . . . 10 |- ((J e. Top /\ S C_ X) -> S C_ (X i^i ((cls` J)` S)))
13		dfin4 2835	. . . . . . . . . 10 |- (X i^i ((cls` J)` S)) = (X \ (X \ ((cls` J)` S)))
14	12, 13	syl6ss 2663	. . . . . . . . 9 |- ((J e. Top /\ S C_ X) -> S C_ (X \ (X \ ((cls` J)` S))))
15		reldisj 2916	. . . . . . . . . 10 |- (S C_ X -> ((S i^i (X \ ((cls` J)` S))) = (/) <-> S C_ (X \ (X \ ((cls` J)` S)))))
16	15	adantl 424	. . . . . . . . 9 |- ((J e. Top /\ S C_ X) -> ((S i^i (X \ ((cls` J)` S))) = (/) <-> S C_ (X \ (X \ ((cls` J)` S)))))
17	14, 16	mpbird 213	. . . . . . . 8 |- ((J e. Top /\ S C_ X) -> (S i^i (X \ ((cls` J)` S))) = (/))
18		nne 2021	. . . . . . . . 9 |- (-. ((X \ ((cls` J)` S)) i^i S) =/= (/) <-> ((X \ ((cls` J)` S)) i^i S) = (/))
19		incom 2787	. . . . . . . . . 10 |- ((X \ ((cls` J)` S)) i^i S) = (S i^i (X \ ((cls` J)` S)))
20	19	eqeq1i 1891	. . . . . . . . 9 |- (((X \ ((cls` J)` S)) i^i S) = (/) <-> (S i^i (X \ ((cls` J)` S))) = (/))
21	18, 20	bitri 190	. . . . . . . 8 |- (-. ((X \ ((cls` J)` S)) i^i S) =/= (/) <-> (S i^i (X \ ((cls` J)` S))) = (/))
22	17, 21	sylibr 217	. . . . . . 7 |- ((J e. Top /\ S C_ X) -> -. ((X \ ((cls` J)` S)) i^i S) =/= (/))
23	22	3adant3 896	. . . . . 6 |- ((J e. Top /\ S C_ X /\ P e. X) -> -. ((X \ ((cls` J)` S)) i^i S) =/= (/))
24	23	adantr 425	. . . . 5 |- (((J e. Top /\ S C_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> -. ((X \ ((cls` J)` S)) i^i S) =/= (/))
25		eleq2 1958	. . . . . . 7 |- (x = (X \ ((cls` J)` S)) -> (P e. x <-> P e. (X \ ((cls` J)` S))))
26		ineq1 2789	. . . . . . . . 9 |- (x = (X \ ((cls` J)` S)) -> (x i^i S) = ((X \ ((cls` J)` S)) i^i S))
27	26	neeq1d 2028	. . . . . . . 8 |- (x = (X \ ((cls` J)` S)) -> ((x i^i S) =/= (/) <-> ((X \ ((cls` J)` S)) i^i S) =/= (/)))
28	27	notbid 673	. . . . . . 7 |- (x = (X \ ((cls` J)` S)) -> (-. (x i^i S) =/= (/) <-> -. ((X \ ((cls` J)` S)) i^i S) =/= (/)))
29	25, 28	anbi12d 690	. . . . . 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) =/= (/))))
30	29	rcla4ev 2381	. . . . 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) =/= (/)))
31	4, 7, 24, 30	syl12anc 1098	. . . 4 |- (((J e. Top /\ S C_ X /\ P e. X) /\ -. P e. ((cls` J)` S)) -> E.x e. J (P e. x /\ -. (x i^i S) =/= (/)))
32		simplll 452	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ (S i^i x) = (/)) -> J e. Top)
33	1	opncld 8950	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ x e. J) -> (X \ x) e. (Clsd` J))
34	33	adantlr 429	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ S C_ X) /\ x e. J) -> (X \ x) e. (Clsd` J))
35	34	adantr 425	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (X \ x) e. (Clsd` J))
36		reldisj 2916	. . . . . . . . . . . . . . . . . 18 |- (S C_ X -> ((S i^i x) = (/) <-> S C_ (X \ x)))
37	36	biimpa 460	. . . . . . . . . . . . . . . . 17 |- ((S C_ X /\ (S i^i x) = (/)) -> S C_ (X \ x))
38	37	adantll 428	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ S C_ X) /\ (S i^i x) = (/)) -> S C_ (X \ x))
39	38	adantlr 429	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ (S i^i x) = (/)) -> S C_ (X \ x))
40	1	clsss2 8979	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ (X \ x) e. (Clsd` J) /\ S C_ (X \ x)) -> ((cls` J)` S) C_ (X \ x))
41	32, 35, 39, 40	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ (S i^i x) = (/)) -> ((cls` J)` S) C_ (X \ x))
42	41	sseld 2619	. . . . . . . . . . . . 13 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (P e. ((cls` J)` S) -> P e. (X \ x)))
43		eldifn 2731	. . . . . . . . . . . . 13 |- (P e. (X \ x) -> -. P e. x)
44	42, 43	syl6 25	. . . . . . . . . . . 12 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (P e. ((cls` J)` S) -> -. P e. x))
45	44	con2d 107	. . . . . . . . . . 11 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ (S i^i x) = (/)) -> (P e. x -> -. P e. ((cls` J)` S)))
46		incom 2787	. . . . . . . . . . . . 13 |- (S i^i x) = (x i^i S)
47	46	eqeq1i 1891	. . . . . . . . . . . 12 |- ((S i^i x) = (/) <-> (x i^i S) = (/))
48		df-ne 2019	. . . . . . . . . . . . 13 |- ((x i^i S) =/= (/) <-> -. (x i^i S) = (/))
49	48	con2bii 238	. . . . . . . . . . . 12 |- ((x i^i S) = (/) <-> -. (x i^i S) =/= (/))
50	47, 49	bitri 190	. . . . . . . . . . 11 |- ((S i^i x) = (/) <-> -. (x i^i S) =/= (/))
51	45, 50	sylan2br 502	. . . . . . . . . 10 |- ((((J e. Top /\ S C_ X) /\ x e. J) /\ -. (x i^i S) =/= (/)) -> (P e. x -> -. P e. ((cls` J)` S)))
52	51	exp31 407	. . . . . . . . 9 |- ((J e. Top /\ S C_ X) -> (x e. J -> (-. (x i^i S) =/= (/) -> (P e. x -> -. P e. ((cls` J)` S)))))
53	52	com34 40	. . . . . . . 8 |- ((J e. Top /\ S C_ X) -> (x e. J -> (P e. x -> (-. (x i^i S) =/= (/) -> -. P e. ((cls` J)` S)))))
54	53	imp4a 391	. . . . . . 7 |- ((J e. Top /\ S C_ X) -> (x e. J -> ((P e. x /\ -. (x i^i S) =/= (/)) -> -. P e. ((cls` J)` S))))
55	54	r19.23adv 2215	. . . . . 6 |- ((J e. Top /\ S C_ X) -> (E.x e. J (P e. x /\ -. (x i^i S) =/= (/)) -> -. P e. ((cls` J)` S)))
56	55	imp 377	. . . . 5 |- (((J e. Top /\ S C_ X) /\ E.x e. J (P e. x /\ -. (x i^i S) =/= (/))) -> -. P e. ((cls` J)` S))
57	56	3adantl3 1034	. . . 4 |- (((J e. Top /\ S C_ X /\ P e. X) /\ E.x e. J (P e. x /\ -. (x i^i S) =/= (/))) -> -. P e. ((cls` J)` S))
58	31, 57	impbida 577	. . 3 |- ((J e. Top /\ S C_ X /\ P e. X) -> (-. P e. ((cls` J)` S) <-> E.x e. J (P e. x /\ -. (x i^i S) =/= (/))))
59		rexanali 2144	. . 3 |- (E.x e. J (P e. x /\ -. (x i^i S) =/= (/)) <-> -. A.x e. J (P e. x -> (x i^i S) =/= (/)))
60	58, 59	syl6bb 595	. 2 |- ((J e. Top /\ S C_ X /\ P e. X) -> (-. P e. ((cls` J)` S) <-> -. A.x e. J (P e. x -> (x i^i S) =/= (/))))
61	60	con4bid 583	1 |- ((J e. Top /\ S C_ X /\ P e. X) -> (P e. ((cls` J)` S) <-> A.x e. J (P e. x -> (x i^i S) =/= (/))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177  ` cfv 3998  Topctop 8857  Clsdccld 8936  clsccl 8938

This theorem is referenced by:  elcls2 8981  clsndisj 8982  elcls3 8987  islp3 14861  flimcls 15588  isfclus 15606

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-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-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  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-fv 4014  df-top 8861  df-cld 8939  df-ntr 8940  df-cls 8941

Copyright terms: Public domain