This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ) ∩ 𝑌 ) )