Metamath Proof Explorer

Theorem fclsrest

Description: The set of cluster points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion fclsrest 
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( J |`t Y ) fClus ( F |`t Y ) ) = ( ( J fClus F ) i^i Y ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> J e. ( TopOn ` X ) )
2 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ Y e. F ) -> Y C_ X )
3 2 3adant1 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> Y C_ X )
4 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ Y C_ X ) -> ( J |`t Y ) e. ( TopOn ` Y ) )
5 1 3 4 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( J |`t Y ) e. ( TopOn ` Y ) )
6 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
7 6 3ad2ant2 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> F e. ( fBas ` X ) )
8 simp3 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> Y e. F )
9 fbncp 
 |-  ( ( F e. ( fBas ` X ) /\ Y e. F ) -> -. ( X \ Y ) e. F )
10 7 8 9 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> -. ( X \ Y ) e. F )
11 simp2 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> F e. ( Fil ` X ) )
12 trfil3 
 |-  ( ( F e. ( Fil ` X ) /\ Y C_ X ) -> ( ( F |`t Y ) e. ( Fil ` Y ) <-> -. ( X \ Y ) e. F ) )
13 11 3 12 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( F |`t Y ) e. ( Fil ` Y ) <-> -. ( X \ Y ) e. F ) )
14 10 13 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( F |`t Y ) e. ( Fil ` Y ) )
15 fclsopn 
 |-  ( ( ( J |`t Y ) e. ( TopOn ` Y ) /\ ( F |`t Y ) e. ( Fil ` Y ) ) -> ( x e. ( ( J |`t Y ) fClus ( F |`t Y ) ) <-> ( x e. Y /\ A. y e. ( J |`t Y ) ( x e. y -> A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) ) ) ) )
16 5 14 15 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( x e. ( ( J |`t Y ) fClus ( F |`t Y ) ) <-> ( x e. Y /\ A. y e. ( J |`t Y ) ( x e. y -> A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) ) ) ) )
17 in32 
 |-  ( ( u i^i s ) i^i Y ) = ( ( u i^i Y ) i^i s )
18 ineq2 
 |-  ( s = t -> ( ( u i^i Y ) i^i s ) = ( ( u i^i Y ) i^i t ) )
19 17 18 syl5eq 
 |-  ( s = t -> ( ( u i^i s ) i^i Y ) = ( ( u i^i Y ) i^i t ) )
20 19 neeq1d 
 |-  ( s = t -> ( ( ( u i^i s ) i^i Y ) =/= (/) <-> ( ( u i^i Y ) i^i t ) =/= (/) ) )
21 20 rspccv 
 |-  ( A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) -> ( t e. F -> ( ( u i^i Y ) i^i t ) =/= (/) ) )
22 inss1 
 |-  ( u i^i Y ) C_ u
23 ssrin 
 |-  ( ( u i^i Y ) C_ u -> ( ( u i^i Y ) i^i t ) C_ ( u i^i t ) )
24 22 23 ax-mp 
 |-  ( ( u i^i Y ) i^i t ) C_ ( u i^i t )
25 ssn0 
 |-  ( ( ( ( u i^i Y ) i^i t ) C_ ( u i^i t ) /\ ( ( u i^i Y ) i^i t ) =/= (/) ) -> ( u i^i t ) =/= (/) )
26 24 25 mpan 
 |-  ( ( ( u i^i Y ) i^i t ) =/= (/) -> ( u i^i t ) =/= (/) )
27 21 26 syl6 
 |-  ( A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) -> ( t e. F -> ( u i^i t ) =/= (/) ) )
28 27 ralrimiv 
 |-  ( A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) -> A. t e. F ( u i^i t ) =/= (/) )
29 11 ad3antrrr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) /\ s e. F ) -> F e. ( Fil ` X ) )
30 simpr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) /\ s e. F ) -> s e. F )
31 8 ad3antrrr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) /\ s e. F ) -> Y e. F )
32 filin 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F /\ Y e. F ) -> ( s i^i Y ) e. F )
33 29 30 31 32 syl3anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) /\ s e. F ) -> ( s i^i Y ) e. F )
34 ineq2 
 |-  ( t = ( s i^i Y ) -> ( u i^i t ) = ( u i^i ( s i^i Y ) ) )
35 inass 
 |-  ( ( u i^i s ) i^i Y ) = ( u i^i ( s i^i Y ) )
36 34 35 eqtr4di 
 |-  ( t = ( s i^i Y ) -> ( u i^i t ) = ( ( u i^i s ) i^i Y ) )
37 36 neeq1d 
 |-  ( t = ( s i^i Y ) -> ( ( u i^i t ) =/= (/) <-> ( ( u i^i s ) i^i Y ) =/= (/) ) )
38 37 rspcv 
 |-  ( ( s i^i Y ) e. F -> ( A. t e. F ( u i^i t ) =/= (/) -> ( ( u i^i s ) i^i Y ) =/= (/) ) )
39 33 38 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) /\ s e. F ) -> ( A. t e. F ( u i^i t ) =/= (/) -> ( ( u i^i s ) i^i Y ) =/= (/) ) )
40 39 ralrimdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) -> ( A. t e. F ( u i^i t ) =/= (/) -> A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) ) )
41 28 40 impbid2 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) -> ( A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) <-> A. t e. F ( u i^i t ) =/= (/) ) )
42 41 imbi2d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) -> ( ( x e. u -> A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) ) <-> ( x e. u -> A. t e. F ( u i^i t ) =/= (/) ) ) )
43 42 ralbidva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( A. u e. J ( x e. u -> A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) ) <-> A. u e. J ( x e. u -> A. t e. F ( u i^i t ) =/= (/) ) ) )
44 vex 
 |-  u e. _V
45 44 inex1 
 |-  ( u i^i Y ) e. _V
46 45 a1i 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ u e. J ) -> ( u i^i Y ) e. _V )
47 elrest 
 |-  ( ( J e. ( TopOn ` X ) /\ Y e. F ) -> ( y e. ( J |`t Y ) <-> E. u e. J y = ( u i^i Y ) ) )
48 47 3adant2 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( y e. ( J |`t Y ) <-> E. u e. J y = ( u i^i Y ) ) )
49 48 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( y e. ( J |`t Y ) <-> E. u e. J y = ( u i^i Y ) ) )
50 eleq2 
 |-  ( y = ( u i^i Y ) -> ( x e. y <-> x e. ( u i^i Y ) ) )
51 elin 
 |-  ( x e. ( u i^i Y ) <-> ( x e. u /\ x e. Y ) )
52 51 rbaib 
 |-  ( x e. Y -> ( x e. ( u i^i Y ) <-> x e. u ) )
53 52 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( x e. ( u i^i Y ) <-> x e. u ) )
54 50 53 sylan9bbr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ y = ( u i^i Y ) ) -> ( x e. y <-> x e. u ) )
55 vex 
 |-  s e. _V
56 55 inex1 
 |-  ( s i^i Y ) e. _V
57 56 a1i 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ s e. F ) -> ( s i^i Y ) e. _V )
58 elrest 
 |-  ( ( F e. ( Fil ` X ) /\ Y e. F ) -> ( z e. ( F |`t Y ) <-> E. s e. F z = ( s i^i Y ) ) )
59 58 3adant1 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( z e. ( F |`t Y ) <-> E. s e. F z = ( s i^i Y ) ) )
60 59 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( z e. ( F |`t Y ) <-> E. s e. F z = ( s i^i Y ) ) )
61 ineq2 
 |-  ( z = ( s i^i Y ) -> ( y i^i z ) = ( y i^i ( s i^i Y ) ) )
62 61 adantl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ z = ( s i^i Y ) ) -> ( y i^i z ) = ( y i^i ( s i^i Y ) ) )
63 62 neeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ z = ( s i^i Y ) ) -> ( ( y i^i z ) =/= (/) <-> ( y i^i ( s i^i Y ) ) =/= (/) ) )
64 57 60 63 ralxfr2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) <-> A. s e. F ( y i^i ( s i^i Y ) ) =/= (/) ) )
65 ineq1 
 |-  ( y = ( u i^i Y ) -> ( y i^i ( s i^i Y ) ) = ( ( u i^i Y ) i^i ( s i^i Y ) ) )
66 inindir 
 |-  ( ( u i^i s ) i^i Y ) = ( ( u i^i Y ) i^i ( s i^i Y ) )
67 65 66 eqtr4di 
 |-  ( y = ( u i^i Y ) -> ( y i^i ( s i^i Y ) ) = ( ( u i^i s ) i^i Y ) )
68 67 neeq1d 
 |-  ( y = ( u i^i Y ) -> ( ( y i^i ( s i^i Y ) ) =/= (/) <-> ( ( u i^i s ) i^i Y ) =/= (/) ) )
69 68 ralbidv 
 |-  ( y = ( u i^i Y ) -> ( A. s e. F ( y i^i ( s i^i Y ) ) =/= (/) <-> A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) ) )
70 64 69 sylan9bb 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ y = ( u i^i Y ) ) -> ( A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) <-> A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) ) )
71 54 70 imbi12d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) /\ y = ( u i^i Y ) ) -> ( ( x e. y -> A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) ) <-> ( x e. u -> A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) ) ) )
72 46 49 71 ralxfr2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( A. y e. ( J |`t Y ) ( x e. y -> A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) ) <-> A. u e. J ( x e. u -> A. s e. F ( ( u i^i s ) i^i Y ) =/= (/) ) ) )
73 1 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> J e. ( TopOn ` X ) )
74 11 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> F e. ( Fil ` X ) )
75 3 sselda 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> x e. X )
76 fclsopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( x e. ( J fClus F ) <-> ( x e. X /\ A. u e. J ( x e. u -> A. t e. F ( u i^i t ) =/= (/) ) ) ) )
77 76 baibd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ x e. X ) -> ( x e. ( J fClus F ) <-> A. u e. J ( x e. u -> A. t e. F ( u i^i t ) =/= (/) ) ) )
78 73 74 75 77 syl21anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( x e. ( J fClus F ) <-> A. u e. J ( x e. u -> A. t e. F ( u i^i t ) =/= (/) ) ) )
79 43 72 78 3bitr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ x e. Y ) -> ( A. y e. ( J |`t Y ) ( x e. y -> A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) ) <-> x e. ( J fClus F ) ) )
80 79 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( x e. Y /\ A. y e. ( J |`t Y ) ( x e. y -> A. z e. ( F |`t Y ) ( y i^i z ) =/= (/) ) ) <-> ( x e. Y /\ x e. ( J fClus F ) ) ) )
81 16 80 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( x e. ( ( J |`t Y ) fClus ( F |`t Y ) ) <-> ( x e. Y /\ x e. ( J fClus F ) ) ) )
82 elin 
 |-  ( x e. ( ( J fClus F ) i^i Y ) <-> ( x e. ( J fClus F ) /\ x e. Y ) )
83 82 biancomi 
 |-  ( x e. ( ( J fClus F ) i^i Y ) <-> ( x e. Y /\ x e. ( J fClus F ) ) )
84 81 83 syl6bbr 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( x e. ( ( J |`t Y ) fClus ( F |`t Y ) ) <-> x e. ( ( J fClus F ) i^i Y ) ) )
85 84 eqrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( J |`t Y ) fClus ( F |`t Y ) ) = ( ( J fClus F ) i^i Y ) )