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 bitr4di
 |-  ( ( 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 ) )