Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elcls Structured version   Visualization version   GIF version

Theorem elcls 21097
 Description: Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.)
Hypothesis
Ref Expression
clscld.1 𝑋 = 𝐽
Assertion
Ref Expression
elcls ((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥𝐽 (𝑃𝑥 → (𝑥𝑆) ≠ ∅)))
Distinct variable groups:   𝑥,𝐽   𝑥,𝑃   𝑥,𝑆   𝑥,𝑋

Proof of Theorem elcls
StepHypRef Expression
1 clscld.1 . . . . . . . 8 𝑋 = 𝐽
21cmclsopn 21086 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽)
323adant3 1125 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽)
43adantr 466 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽)
5 eldif 3731 . . . . . . 7 (𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ↔ (𝑃𝑋 ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
65biimpri 218 . . . . . 6 ((𝑃𝑋 ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))
763ad2antl3 1201 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))
8 simpr 471 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆𝑋)
91sscls 21080 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
108, 9ssind 3983 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ⊆ (𝑋 ∩ ((cls‘𝐽)‘𝑆)))
11 dfin4 4014 . . . . . . . . . 10 (𝑋 ∩ ((cls‘𝐽)‘𝑆)) = (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))
1210, 11syl6sseq 3798 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ⊆ (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆))))
13 reldisj 4161 . . . . . . . . . 10 (𝑆𝑋 → ((𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅ ↔ 𝑆 ⊆ (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))))
1413adantl 467 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅ ↔ 𝑆 ⊆ (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))))
1512, 14mpbird 247 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅)
16 nne 2946 . . . . . . . . 9 (¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅ ↔ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) = ∅)
17 incom 3954 . . . . . . . . . 10 ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) = (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))
1817eqeq1i 2775 . . . . . . . . 9 (((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) = ∅ ↔ (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅)
1916, 18bitri 264 . . . . . . . 8 (¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅ ↔ (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅)
2015, 19sylibr 224 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)
21203adant3 1125 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) → ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)
2221adantr 466 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)
23 eleq2 2838 . . . . . . 7 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → (𝑃𝑥𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆))))
24 ineq1 3956 . . . . . . . . 9 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → (𝑥𝑆) = ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆))
2524neeq1d 3001 . . . . . . . 8 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → ((𝑥𝑆) ≠ ∅ ↔ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅))
2625notbid 307 . . . . . . 7 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → (¬ (𝑥𝑆) ≠ ∅ ↔ ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅))
2723, 26anbi12d 608 . . . . . 6 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → ((𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∧ ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)))
2827rspcev 3458 . . . . 5 (((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽 ∧ (𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∧ ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)) → ∃𝑥𝐽 (𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅))
294, 7, 22, 28syl12anc 1473 . . . 4 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑥𝐽 (𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅))
30 incom 3954 . . . . . . . . . . . . 13 (𝑆𝑥) = (𝑥𝑆)
3130eqeq1i 2775 . . . . . . . . . . . 12 ((𝑆𝑥) = ∅ ↔ (𝑥𝑆) = ∅)
32 df-ne 2943 . . . . . . . . . . . . 13 ((𝑥𝑆) ≠ ∅ ↔ ¬ (𝑥𝑆) = ∅)
3332con2bii 346 . . . . . . . . . . . 12 ((𝑥𝑆) = ∅ ↔ ¬ (𝑥𝑆) ≠ ∅)
3431, 33bitri 264 . . . . . . . . . . 11 ((𝑆𝑥) = ∅ ↔ ¬ (𝑥𝑆) ≠ ∅)
351opncld 21057 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑥𝐽) → (𝑋𝑥) ∈ (Clsd‘𝐽))
3635adantlr 686 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) → (𝑋𝑥) ∈ (Clsd‘𝐽))
3736adantr 466 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) ∧ (𝑆𝑥) = ∅) → (𝑋𝑥) ∈ (Clsd‘𝐽))
38 reldisj 4161 . . . . . . . . . . . . . . . . . 18 (𝑆𝑋 → ((𝑆𝑥) = ∅ ↔ 𝑆 ⊆ (𝑋𝑥)))
3938biimpa 462 . . . . . . . . . . . . . . . . 17 ((𝑆𝑋 ∧ (𝑆𝑥) = ∅) → 𝑆 ⊆ (𝑋𝑥))
4039adantll 685 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ (𝑆𝑥) = ∅) → 𝑆 ⊆ (𝑋𝑥))
4140adantlr 686 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) ∧ (𝑆𝑥) = ∅) → 𝑆 ⊆ (𝑋𝑥))
421clsss2 21096 . . . . . . . . . . . . . . 15 (((𝑋𝑥) ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ (𝑋𝑥)) → ((cls‘𝐽)‘𝑆) ⊆ (𝑋𝑥))
4337, 41, 42syl2anc 565 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) ∧ (𝑆𝑥) = ∅) → ((cls‘𝐽)‘𝑆) ⊆ (𝑋𝑥))
4443sseld 3749 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) ∧ (𝑆𝑥) = ∅) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → 𝑃 ∈ (𝑋𝑥)))
45 eldifn 3882 . . . . . . . . . . . . 13 (𝑃 ∈ (𝑋𝑥) → ¬ 𝑃𝑥)
4644, 45syl6 35 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) ∧ (𝑆𝑥) = ∅) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → ¬ 𝑃𝑥))
4746con2d 131 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) ∧ (𝑆𝑥) = ∅) → (𝑃𝑥 → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
4834, 47sylan2br 574 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑥𝐽) ∧ ¬ (𝑥𝑆) ≠ ∅) → (𝑃𝑥 → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
4948exp31 406 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑥𝐽 → (¬ (𝑥𝑆) ≠ ∅ → (𝑃𝑥 → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)))))
5049com34 91 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑥𝐽 → (𝑃𝑥 → (¬ (𝑥𝑆) ≠ ∅ → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)))))
5150imp4a 409 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑥𝐽 → ((𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))))
5251rexlimdv 3177 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∃𝑥𝐽 (𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
5352imp 393 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ ∃𝑥𝐽 (𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅)) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))
54533adantl3 1172 . . . 4 (((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) ∧ ∃𝑥𝐽 (𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅)) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))
5529, 54impbida 794 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) → (¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑥𝐽 (𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅)))
56 rexanali 3145 . . 3 (∃𝑥𝐽 (𝑃𝑥 ∧ ¬ (𝑥𝑆) ≠ ∅) ↔ ¬ ∀𝑥𝐽 (𝑃𝑥 → (𝑥𝑆) ≠ ∅))
5755, 56syl6bb 276 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) → (¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ¬ ∀𝑥𝐽 (𝑃𝑥 → (𝑥𝑆) ≠ ∅)))
5857con4bid 306 1 ((𝐽 ∈ Top ∧ 𝑆𝑋𝑃𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥𝐽 (𝑃𝑥 → (𝑥𝑆) ≠ ∅)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1070   = wceq 1630   ∈ wcel 2144   ≠ wne 2942  ∀wral 3060  ∃wrex 3061   ∖ cdif 3718   ∩ cin 3720   ⊆ wss 3721  ∅c0 4061  ∪ cuni 4572  ‘cfv 6031  Topctop 20917  Clsdccld 21040  clsccl 21042 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-iin 4655  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-top 20918  df-cld 21043  df-ntr 21044  df-cls 21045 This theorem is referenced by:  elcls2  21098  clsndisj  21099  elcls3  21107  neindisj2  21147  islp3  21170  lmcls  21326  1stccnp  21485  txcls  21627  dfac14lem  21640  fclsopn  22037  metdseq0  22876  qndenserrn  41030
 Copyright terms: Public domain W3C validator