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