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 = U. J
Assertion 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 ) =/= (/) ) ) )

Proof

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