Metamath Proof Explorer


Theorem elcls

Description: Membership in a closure. Theorem 6.5(a) of Munkres p. 95. (Contributed by NM, 22-Feb-2007)

Ref Expression
Hypothesis clscld.1 X = J
Assertion elcls J Top S X P X P cls J S x J P x x S

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 1 cmclsopn J Top S X X cls J S J
3 2 3adant3 J Top S X P X X cls J S J
4 3 adantr J Top S X P X ¬ P cls J S X cls J S J
5 eldif P X cls J S P X ¬ P cls J S
6 5 biimpri P X ¬ P cls J S P X cls J S
7 6 3ad2antl3 J Top S X P X ¬ P cls J S P X cls J S
8 simpr J Top S X S X
9 1 sscls J Top S X S cls J S
10 8 9 ssind J Top S X S X cls J S
11 dfin4 X cls J S = X X cls J S
12 10 11 sseqtrdi J Top S X S X X cls J S
13 reldisj S X S X cls J S = S X X cls J S
14 13 adantl J Top S X S X cls J S = S X X cls J S
15 12 14 mpbird J Top S X S X cls J S =
16 nne ¬ X cls J S S X cls J S S =
17 incom X cls J S S = S X cls J S
18 17 eqeq1i X cls J S S = S X cls J S =
19 16 18 bitri ¬ X cls J S S S X cls J S =
20 15 19 sylibr J Top S X ¬ X cls J S S
21 20 3adant3 J Top S X P X ¬ X cls J S S
22 21 adantr J Top S X P X ¬ P cls J S ¬ X cls J S S
23 eleq2 x = X cls J S P x P X cls J S
24 ineq1 x = X cls J S x S = X cls J S S
25 24 neeq1d x = X cls J S x S X cls J S S
26 25 notbid x = X cls J S ¬ x S ¬ X cls J S S
27 23 26 anbi12d x = X cls J S P x ¬ x S P X cls J S ¬ X cls J S S
28 27 rspcev X cls J S J P X cls J S ¬ X cls J S S x J P x ¬ x S
29 4 7 22 28 syl12anc J Top S X P X ¬ P cls J S x J P x ¬ x S
30 incom S x = x S
31 30 eqeq1i S x = x S =
32 df-ne x S ¬ x S =
33 32 con2bii x S = ¬ x S
34 31 33 bitri S x = ¬ x S
35 1 opncld J Top x J X x Clsd J
36 35 adantlr J Top S X x J X x Clsd J
37 reldisj S X S x = S X x
38 37 biimpa S X S x = S X x
39 38 ad4ant24 J Top S X x J S x = S X x
40 1 clsss2 X x Clsd J S X x cls J S X x
41 36 39 40 syl2an2r J Top S X x J S x = cls J S X x
42 41 sseld J Top S X x J S x = P cls J S P X x
43 eldifn P X x ¬ P x
44 42 43 syl6 J Top S X x J S x = P cls J S ¬ P x
45 44 con2d J Top S X x J S x = P x ¬ P cls J S
46 34 45 sylan2br J Top S X x J ¬ x S P x ¬ P cls J S
47 46 exp31 J Top S X x J ¬ x S P x ¬ P cls J S
48 47 com34 J Top S X x J P x ¬ x S ¬ P cls J S
49 48 imp4a J Top S X x J P x ¬ x S ¬ P cls J S
50 49 rexlimdv J Top S X x J P x ¬ x S ¬ P cls J S
51 50 imp J Top S X x J P x ¬ x S ¬ P cls J S
52 51 3adantl3 J Top S X P X x J P x ¬ x S ¬ P cls J S
53 29 52 impbida J Top S X P X ¬ P cls J S x J P x ¬ x S
54 rexanali x J P x ¬ x S ¬ x J P x x S
55 53 54 syl6bb J Top S X P X ¬ P cls J S ¬ x J P x x S
56 55 con4bid J Top S X P X P cls J S x J P x x S