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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( ( 𝐽t 𝑌 ) fLim ( 𝐹t 𝑌 ) ) = ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 filelss ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → 𝑌𝑋 )
3 2 3adant1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → 𝑌𝑋 )
4 resttopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( 𝐽t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
5 1 3 4 syl2anc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝐽t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
6 filfbas ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
7 6 3ad2ant2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
8 simp3 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → 𝑌𝐹 )
9 fbncp ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ¬ ( 𝑋𝑌 ) ∈ 𝐹 )
10 7 8 9 syl2anc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ¬ ( 𝑋𝑌 ) ∈ 𝐹 )
11 simp2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
12 trfil3 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝑋 ) → ( ( 𝐹t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ↔ ¬ ( 𝑋𝑌 ) ∈ 𝐹 ) )
13 11 3 12 syl2anc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( ( 𝐹t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ↔ ¬ ( 𝑋𝑌 ) ∈ 𝐹 ) )
14 10 13 mpbird ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝐹t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) )
15 flimopn ( ( ( 𝐽t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝐹t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑥 ∈ ( ( 𝐽t 𝑌 ) fLim ( 𝐹t 𝑌 ) ) ↔ ( 𝑥𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽t 𝑌 ) ( 𝑥𝑦𝑦 ∈ ( 𝐹t 𝑌 ) ) ) ) )
16 5 14 15 syl2anc ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝑥 ∈ ( ( 𝐽t 𝑌 ) fLim ( 𝐹t 𝑌 ) ) ↔ ( 𝑥𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽t 𝑌 ) ( 𝑥𝑦𝑦 ∈ ( 𝐹t 𝑌 ) ) ) ) )
17 simpll2 ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
18 simpll3 ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → 𝑌𝐹 )
19 elrestr ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹𝑧𝐹 ) → ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) )
20 19 3expia ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝑧𝐹 → ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) )
21 17 18 20 syl2anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( 𝑧𝐹 → ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) )
22 trfilss ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝐹t 𝑌 ) ⊆ 𝐹 )
23 17 18 22 syl2anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( 𝐹t 𝑌 ) ⊆ 𝐹 )
24 23 sseld ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) → ( 𝑧𝑌 ) ∈ 𝐹 ) )
25 inss1 ( 𝑧𝑌 ) ⊆ 𝑧
26 25 a1i ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( 𝑧𝑌 ) ⊆ 𝑧 )
27 simpl1 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
28 toponss ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧𝐽 ) → 𝑧𝑋 )
29 27 28 sylan ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → 𝑧𝑋 )
30 filss ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑧𝑌 ) ∈ 𝐹𝑧𝑋 ∧ ( 𝑧𝑌 ) ⊆ 𝑧 ) ) → 𝑧𝐹 )
31 30 3exp2 ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑧𝑌 ) ∈ 𝐹 → ( 𝑧𝑋 → ( ( 𝑧𝑌 ) ⊆ 𝑧𝑧𝐹 ) ) ) )
32 31 com24 ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑧𝑌 ) ⊆ 𝑧 → ( 𝑧𝑋 → ( ( 𝑧𝑌 ) ∈ 𝐹𝑧𝐹 ) ) ) )
33 17 26 29 32 syl3c ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( ( 𝑧𝑌 ) ∈ 𝐹𝑧𝐹 ) )
34 24 33 syld ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) → 𝑧𝐹 ) )
35 21 34 impbid ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( 𝑧𝐹 ↔ ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) )
36 35 imbi2d ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( ( 𝑥𝑧𝑧𝐹 ) ↔ ( 𝑥𝑧 → ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) ) )
37 36 ralbidva ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → ( ∀ 𝑧𝐽 ( 𝑥𝑧𝑧𝐹 ) ↔ ∀ 𝑧𝐽 ( 𝑥𝑧 → ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) ) )
38 simpl2 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
39 3 sselda ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → 𝑥𝑋 )
40 flimopn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥𝑋 ∧ ∀ 𝑧𝐽 ( 𝑥𝑧𝑧𝐹 ) ) ) )
41 40 baibd ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥𝑋 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑧𝐽 ( 𝑥𝑧𝑧𝐹 ) ) )
42 27 38 39 41 syl21anc ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑧𝐽 ( 𝑥𝑧𝑧𝐹 ) ) )
43 vex 𝑧 ∈ V
44 43 inex1 ( 𝑧𝑌 ) ∈ V
45 44 a1i ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑧𝐽 ) → ( 𝑧𝑌 ) ∈ V )
46 simpl3 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → 𝑌𝐹 )
47 elrest ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝑦 ∈ ( 𝐽t 𝑌 ) ↔ ∃ 𝑧𝐽 𝑦 = ( 𝑧𝑌 ) ) )
48 27 46 47 syl2anc ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → ( 𝑦 ∈ ( 𝐽t 𝑌 ) ↔ ∃ 𝑧𝐽 𝑦 = ( 𝑧𝑌 ) ) )
49 eleq2 ( 𝑦 = ( 𝑧𝑌 ) → ( 𝑥𝑦𝑥 ∈ ( 𝑧𝑌 ) ) )
50 elin ( 𝑥 ∈ ( 𝑧𝑌 ) ↔ ( 𝑥𝑧𝑥𝑌 ) )
51 50 rbaib ( 𝑥𝑌 → ( 𝑥 ∈ ( 𝑧𝑌 ) ↔ 𝑥𝑧 ) )
52 51 adantl ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → ( 𝑥 ∈ ( 𝑧𝑌 ) ↔ 𝑥𝑧 ) )
53 49 52 sylan9bbr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑦 = ( 𝑧𝑌 ) ) → ( 𝑥𝑦𝑥𝑧 ) )
54 eleq1 ( 𝑦 = ( 𝑧𝑌 ) → ( 𝑦 ∈ ( 𝐹t 𝑌 ) ↔ ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) )
55 54 adantl ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑦 = ( 𝑧𝑌 ) ) → ( 𝑦 ∈ ( 𝐹t 𝑌 ) ↔ ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) )
56 53 55 imbi12d ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) ∧ 𝑦 = ( 𝑧𝑌 ) ) → ( ( 𝑥𝑦𝑦 ∈ ( 𝐹t 𝑌 ) ) ↔ ( 𝑥𝑧 → ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) ) )
57 45 48 56 ralxfr2d ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐽t 𝑌 ) ( 𝑥𝑦𝑦 ∈ ( 𝐹t 𝑌 ) ) ↔ ∀ 𝑧𝐽 ( 𝑥𝑧 → ( 𝑧𝑌 ) ∈ ( 𝐹t 𝑌 ) ) ) )
58 37 42 57 3bitr4d ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) ∧ 𝑥𝑌 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑦 ∈ ( 𝐽t 𝑌 ) ( 𝑥𝑦𝑦 ∈ ( 𝐹t 𝑌 ) ) ) )
59 58 pm5.32da ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( ( 𝑥𝑌𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ↔ ( 𝑥𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽t 𝑌 ) ( 𝑥𝑦𝑦 ∈ ( 𝐹t 𝑌 ) ) ) ) )
60 16 59 bitr4d ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝑥 ∈ ( ( 𝐽t 𝑌 ) fLim ( 𝐹t 𝑌 ) ) ↔ ( 𝑥𝑌𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ) )
61 ancom ( ( 𝑥𝑌𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ↔ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥𝑌 ) )
62 elin ( 𝑥 ∈ ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥𝑌 ) )
63 61 62 bitr4i ( ( 𝑥𝑌𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ↔ 𝑥 ∈ ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) )
64 60 63 bitrdi ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( 𝑥 ∈ ( ( 𝐽t 𝑌 ) fLim ( 𝐹t 𝑌 ) ) ↔ 𝑥 ∈ ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) ) )
65 64 eqrdv ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌𝐹 ) → ( ( 𝐽t 𝑌 ) fLim ( 𝐹t 𝑌 ) ) = ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) )