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 syl6bb 
 |-  ( ( 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 ) =/= (/) ) ) )