Metamath Proof Explorer


Theorem flimrest

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

Ref Expression
Assertion flimrest J TopOn X F Fil X Y F J 𝑡 Y fLim F 𝑡 Y = J fLim 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 flimopn J 𝑡 Y TopOn Y F 𝑡 Y Fil Y x J 𝑡 Y fLim F 𝑡 Y x Y y J 𝑡 Y x y y F 𝑡 Y
16 5 14 15 syl2anc J TopOn X F Fil X Y F x J 𝑡 Y fLim F 𝑡 Y x Y y J 𝑡 Y x y y F 𝑡 Y
17 simpll2 J TopOn X F Fil X Y F x Y z J F Fil X
18 simpll3 J TopOn X F Fil X Y F x Y z J Y F
19 elrestr F Fil X Y F z F z Y F 𝑡 Y
20 19 3expia F Fil X Y F z F z Y F 𝑡 Y
21 17 18 20 syl2anc J TopOn X F Fil X Y F x Y z J z F z Y F 𝑡 Y
22 trfilss F Fil X Y F F 𝑡 Y F
23 17 18 22 syl2anc J TopOn X F Fil X Y F x Y z J F 𝑡 Y F
24 23 sseld J TopOn X F Fil X Y F x Y z J z Y F 𝑡 Y z Y F
25 inss1 z Y z
26 25 a1i J TopOn X F Fil X Y F x Y z J z Y z
27 simpl1 J TopOn X F Fil X Y F x Y J TopOn X
28 toponss J TopOn X z J z X
29 27 28 sylan J TopOn X F Fil X Y F x Y z J z X
30 filss F Fil X z Y F z X z Y z z F
31 30 3exp2 F Fil X z Y F z X z Y z z F
32 31 com24 F Fil X z Y z z X z Y F z F
33 17 26 29 32 syl3c J TopOn X F Fil X Y F x Y z J z Y F z F
34 24 33 syld J TopOn X F Fil X Y F x Y z J z Y F 𝑡 Y z F
35 21 34 impbid J TopOn X F Fil X Y F x Y z J z F z Y F 𝑡 Y
36 35 imbi2d J TopOn X F Fil X Y F x Y z J x z z F x z z Y F 𝑡 Y
37 36 ralbidva J TopOn X F Fil X Y F x Y z J x z z F z J x z z Y F 𝑡 Y
38 simpl2 J TopOn X F Fil X Y F x Y F Fil X
39 3 sselda J TopOn X F Fil X Y F x Y x X
40 flimopn J TopOn X F Fil X x J fLim F x X z J x z z F
41 40 baibd J TopOn X F Fil X x X x J fLim F z J x z z F
42 27 38 39 41 syl21anc J TopOn X F Fil X Y F x Y x J fLim F z J x z z F
43 vex z V
44 43 inex1 z Y V
45 44 a1i J TopOn X F Fil X Y F x Y z J z Y V
46 simpl3 J TopOn X F Fil X Y F x Y Y F
47 elrest J TopOn X Y F y J 𝑡 Y z J y = z Y
48 27 46 47 syl2anc J TopOn X F Fil X Y F x Y y J 𝑡 Y z J y = z Y
49 eleq2 y = z Y x y x z Y
50 elin x z Y x z x Y
51 50 rbaib x Y x z Y x z
52 51 adantl J TopOn X F Fil X Y F x Y x z Y x z
53 49 52 sylan9bbr J TopOn X F Fil X Y F x Y y = z Y x y x z
54 eleq1 y = z Y y F 𝑡 Y z Y F 𝑡 Y
55 54 adantl J TopOn X F Fil X Y F x Y y = z Y y F 𝑡 Y z Y F 𝑡 Y
56 53 55 imbi12d J TopOn X F Fil X Y F x Y y = z Y x y y F 𝑡 Y x z z Y F 𝑡 Y
57 45 48 56 ralxfr2d J TopOn X F Fil X Y F x Y y J 𝑡 Y x y y F 𝑡 Y z J x z z Y F 𝑡 Y
58 37 42 57 3bitr4d J TopOn X F Fil X Y F x Y x J fLim F y J 𝑡 Y x y y F 𝑡 Y
59 58 pm5.32da J TopOn X F Fil X Y F x Y x J fLim F x Y y J 𝑡 Y x y y F 𝑡 Y
60 16 59 bitr4d J TopOn X F Fil X Y F x J 𝑡 Y fLim F 𝑡 Y x Y x J fLim F
61 ancom x Y x J fLim F x J fLim F x Y
62 elin x J fLim F Y x J fLim F x Y
63 61 62 bitr4i x Y x J fLim F x J fLim F Y
64 60 63 bitrdi J TopOn X F Fil X Y F x J 𝑡 Y fLim F 𝑡 Y x J fLim F Y
65 64 eqrdv J TopOn X F Fil X Y F J 𝑡 Y fLim F 𝑡 Y = J fLim F Y