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 TopOn X F Fil X Y F J 𝑡 Y fClus F 𝑡 Y = J fClus F Y

Proof

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