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 syl5eq ( 𝑠 = 𝑡 → ( ( 𝑢𝑠 ) ∩ 𝑌 ) = ( ( 𝑢𝑌 ) ∩ 𝑡 ) )
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 𝐹 ) ∩ 𝑌 ) )