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

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

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 fclsopn ⊢ ( ( ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fClus ( 𝐹 ↾t 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) ) ) )
16 5 14 15 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fClus ( 𝐹 ↾t 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) ) ) )
17 in32 ⊢ ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) = ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑠 )
18 ineq2 ⊢ ( 𝑠 = 𝑡 → ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑠 ) = ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) )
19 17 18 eqtrid ⊢ ( 𝑠 = 𝑡 → ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) = ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) )
20 19 neeq1d ⊢ ( 𝑠 = 𝑡 → ( ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ↔ ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) ≠ ∅ ) )
21 20 rspccv ⊢ ( ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ → ( 𝑡 ∈ 𝐹 → ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) ≠ ∅ ) )
22 inss1 ⊢ ( 𝑢 ∩ 𝑌 ) ⊆ 𝑢
23 ssrin ⊢ ( ( 𝑢 ∩ 𝑌 ) ⊆ 𝑢 → ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) ⊆ ( 𝑢 ∩ 𝑡 ) )
24 22 23 ax-mp ⊢ ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) ⊆ ( 𝑢 ∩ 𝑡 )
25 ssn0 ⊢ ( ( ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) ⊆ ( 𝑢 ∩ 𝑡 ) ∧ ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) ≠ ∅ ) → ( 𝑢 ∩ 𝑡 ) ≠ ∅ )
26 24 25 mpan ⊢ ( ( ( 𝑢 ∩ 𝑌 ) ∩ 𝑡 ) ≠ ∅ → ( 𝑢 ∩ 𝑡 ) ≠ ∅ )
27 21 26 syl6 ⊢ ( ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ → ( 𝑡 ∈ 𝐹 → ( 𝑢 ∩ 𝑡 ) ≠ ∅ ) )
28 27 ralrimiv ⊢ ( ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ → ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ )
29 11 ad3antrrr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
30 simpr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ∈ 𝐹 )
31 8 ad3antrrr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐹 ) → 𝑌 ∈ 𝐹 )
32 filin ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑠 ∩ 𝑌 ) ∈ 𝐹 )
33 29 30 31 32 syl3anc ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐹 ) → ( 𝑠 ∩ 𝑌 ) ∈ 𝐹 )
34 ineq2 ⊢ ( 𝑡 = ( 𝑠 ∩ 𝑌 ) → ( 𝑢 ∩ 𝑡 ) = ( 𝑢 ∩ ( 𝑠 ∩ 𝑌 ) ) )
35 inass ⊢ ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) = ( 𝑢 ∩ ( 𝑠 ∩ 𝑌 ) )
36 34 35 eqtr4di ⊢ ( 𝑡 = ( 𝑠 ∩ 𝑌 ) → ( 𝑢 ∩ 𝑡 ) = ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) )
37 36 neeq1d ⊢ ( 𝑡 = ( 𝑠 ∩ 𝑌 ) → ( ( 𝑢 ∩ 𝑡 ) ≠ ∅ ↔ ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) )
38 37 rspcv ⊢ ( ( 𝑠 ∩ 𝑌 ) ∈ 𝐹 → ( ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ → ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) )
39 33 38 syl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐹 ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ → ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) )
40 39 ralrimdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) )
41 28 40 impbid2 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) → ( ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ↔ ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ ) )
42 41 imbi2d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑢 → ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) ↔ ( 𝑥 ∈ 𝑢 → ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ ) ) )
43 42 ralbidva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ ) ) )
44 vex ⊢ 𝑢 ∈ V
45 44 inex1 ⊢ ( 𝑢 ∩ 𝑌 ) ∈ V
46 45 a1i ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) → ( 𝑢 ∩ 𝑌 ) ∈ V )
47 elrest ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑦 = ( 𝑢 ∩ 𝑌 ) ) )
48 47 3adant2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑦 = ( 𝑢 ∩ 𝑌 ) ) )
49 48 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑦 = ( 𝑢 ∩ 𝑌 ) ) )
50 eleq2 ⊢ ( 𝑦 = ( 𝑢 ∩ 𝑌 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑢 ∩ 𝑌 ) ) )
51 elin ⊢ ( 𝑥 ∈ ( 𝑢 ∩ 𝑌 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑌 ) )
52 51 rbaib ⊢ ( 𝑥 ∈ 𝑌 → ( 𝑥 ∈ ( 𝑢 ∩ 𝑌 ) ↔ 𝑥 ∈ 𝑢 ) )
53 52 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ ( 𝑢 ∩ 𝑌 ) ↔ 𝑥 ∈ 𝑢 ) )
54 50 53 sylan9bbr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑦 = ( 𝑢 ∩ 𝑌 ) ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑢 ) )
55 vex ⊢ 𝑠 ∈ V
56 55 inex1 ⊢ ( 𝑠 ∩ 𝑌 ) ∈ V
57 56 a1i ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑠 ∈ 𝐹 ) → ( 𝑠 ∩ 𝑌 ) ∈ V )
58 elrest ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ↔ ∃ 𝑠 ∈ 𝐹 𝑧 = ( 𝑠 ∩ 𝑌 ) ) )
59 58 3adant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ↔ ∃ 𝑠 ∈ 𝐹 𝑧 = ( 𝑠 ∩ 𝑌 ) ) )
60 59 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ↔ ∃ 𝑠 ∈ 𝐹 𝑧 = ( 𝑠 ∩ 𝑌 ) ) )
61 ineq2 ⊢ ( 𝑧 = ( 𝑠 ∩ 𝑌 ) → ( 𝑦 ∩ 𝑧 ) = ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) )
62 61 adantl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 = ( 𝑠 ∩ 𝑌 ) ) → ( 𝑦 ∩ 𝑧 ) = ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) )
63 62 neeq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 = ( 𝑠 ∩ 𝑌 ) ) → ( ( 𝑦 ∩ 𝑧 ) ≠ ∅ ↔ ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) ≠ ∅ ) )
64 57 60 63 ralxfr2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐹 ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) ≠ ∅ ) )
65 ineq1 ⊢ ( 𝑦 = ( 𝑢 ∩ 𝑌 ) → ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) = ( ( 𝑢 ∩ 𝑌 ) ∩ ( 𝑠 ∩ 𝑌 ) ) )
66 inindir ⊢ ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) = ( ( 𝑢 ∩ 𝑌 ) ∩ ( 𝑠 ∩ 𝑌 ) )
67 65 66 eqtr4di ⊢ ( 𝑦 = ( 𝑢 ∩ 𝑌 ) → ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) = ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) )
68 67 neeq1d ⊢ ( 𝑦 = ( 𝑢 ∩ 𝑌 ) → ( ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) ≠ ∅ ↔ ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) )
69 68 ralbidv ⊢ ( 𝑦 = ( 𝑢 ∩ 𝑌 ) → ( ∀ 𝑠 ∈ 𝐹 ( 𝑦 ∩ ( 𝑠 ∩ 𝑌 ) ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) )
70 64 69 sylan9bb ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑦 = ( 𝑢 ∩ 𝑌 ) ) → ( ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) )
71 54 70 imbi12d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑦 = ( 𝑢 ∩ 𝑌 ) ) → ( ( 𝑥 ∈ 𝑦 → ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) ↔ ( 𝑥 ∈ 𝑢 → ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) ) )
72 46 49 71 ralxfr2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∀ 𝑠 ∈ 𝐹 ( ( 𝑢 ∩ 𝑠 ) ∩ 𝑌 ) ≠ ∅ ) ) )
73 1 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
74 11 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
75 3 sselda ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
76 fclsopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ ) ) ) )
77 76 baibd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ ) ) )
78 73 74 75 77 syl21anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∀ 𝑡 ∈ 𝐹 ( 𝑢 ∩ 𝑡 ) ≠ ∅ ) ) )
79 43 72 78 3bitr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) ↔ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) )
80 79 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝑥 ∈ 𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → ∀ 𝑧 ∈ ( 𝐹 ↾t 𝑌 ) ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ) )
81 16 80 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fClus ( 𝐹 ↾t 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ) )
82 elin ⊢ ( 𝑥 ∈ ( ( 𝐽 fClus 𝐹 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) )
83 82 biancomi ⊢ ( 𝑥 ∈ ( ( 𝐽 fClus 𝐹 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) )
84 81 83 bitr4di ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fClus ( 𝐹 ↾t 𝑌 ) ) ↔ 𝑥 ∈ ( ( 𝐽 fClus 𝐹 ) ∩ 𝑌 ) ) )
85 84 eqrdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝐽 ↾t 𝑌 ) fClus ( 𝐹 ↾t 𝑌 ) ) = ( ( 𝐽 fClus 𝐹 ) ∩ 𝑌 ) )