Metamath Proof Explorer

Theorem fclscf

Description: Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclscf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 simplr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
3 fclstopon ⊢ ( 𝑥 ∈ ( 𝐾 fClus 𝑓 ) → ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) )
4 3 ad2antll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) )
5 2 4 mpbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
6 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → 𝐽 ⊆ 𝐾 )
7 fclsss1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) )
8 1 5 6 7 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) )
9 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → 𝑥 ∈ ( 𝐾 fClus 𝑓 ) )
10 8 9 sseldd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( 𝐾 fClus 𝑓 ) ) ) → 𝑥 ∈ ( 𝐽 fClus 𝑓 ) )
11 10 expr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( 𝐾 fClus 𝑓 ) → 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ) )
12 11 ssrdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) )
13 12 ralrimivw ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) )
14 simpllr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
15 toponmax ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐾 )
16 ssid ⊢ 𝑋 ⊆ 𝑋
17 eleq2 ⊢ ( 𝑢 = 𝑋 → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ 𝑋 ) )
18 sseq1 ⊢ ( 𝑢 = 𝑋 → ( 𝑢 ⊆ 𝑋 ↔ 𝑋 ⊆ 𝑋 ) )
19 17 18 anbi12d ⊢ ( 𝑢 = 𝑋 → ( ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑋 ⊆ 𝑋 ) ) )
20 19 rspcev ⊢ ( ( 𝑋 ∈ 𝐾 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑋 ⊆ 𝑋 ) ) → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) )
21 16 20 mpanr2 ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) )
22 21 ex ⊢ ( 𝑋 ∈ 𝐾 → ( 𝑦 ∈ 𝑋 → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) ) )
23 14 15 22 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑦 ∈ 𝑋 → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) ) )
24 eleq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑋 ) )
25 sseq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑢 ⊆ 𝑥 ↔ 𝑢 ⊆ 𝑋 ) )
26 25 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ↔ ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) ) )
27 26 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ↔ ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) ) )
28 24 27 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 ∈ 𝑥 → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) ↔ ( 𝑦 ∈ 𝑋 → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋 ) ) ) )
29 23 28 syl5ibrcom ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 = 𝑋 → ( 𝑦 ∈ 𝑥 → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) ) )
30 simplll ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
31 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝑥 ∈ 𝐽 )
32 simprrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝑦 ∈ 𝑥 )
33 supnfcls ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑦 ∈ ( 𝐽 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) )
34 30 31 32 33 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ¬ 𝑦 ∈ ( 𝐽 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) )
35 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 )
36 30 31 35 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝑥 ⊆ 𝑋 )
37 36 32 sseldd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝑦 ∈ 𝑋 )
38 simpllr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
39 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
40 30 39 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝑋 ∈ 𝐽 )
41 difssd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 )
42 simprrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → 𝑥 ≠ 𝑋 )
43 pssdifn0 ⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑥 ≠ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ≠ ∅ )
44 36 42 43 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( 𝑋 ∖ 𝑥 ) ≠ ∅ )
45 supfil ⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) ≠ ∅ ) → { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ∈ ( Fil ‘ 𝑋 ) )
46 40 41 44 45 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ∈ ( Fil ‘ 𝑋 ) )
47 fclsopn ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑦 ∈ ( 𝐾 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ↔ ( 𝑦 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 → ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) ) ) )
48 38 46 47 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( 𝑦 ∈ ( 𝐾 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ↔ ( 𝑦 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 → ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) ) ) )
49 37 48 mpbirand ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( 𝑦 ∈ ( 𝐾 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ↔ ∀ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 → ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) ) )
50 oveq2 ⊢ ( 𝑓 = { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } → ( 𝐾 fClus 𝑓 ) = ( 𝐾 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) )
51 oveq2 ⊢ ( 𝑓 = { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } → ( 𝐽 fClus 𝑓 ) = ( 𝐽 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) )
52 50 51 sseq12d ⊢ ( 𝑓 = { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } → ( ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ↔ ( 𝐾 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ⊆ ( 𝐽 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ) )
53 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) )
54 52 53 46 rspcdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( 𝐾 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ⊆ ( 𝐽 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) )
55 54 sseld ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( 𝑦 ∈ ( 𝐾 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) → 𝑦 ∈ ( 𝐽 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ) )
56 49 55 sylbird ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( ∀ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 → ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) → 𝑦 ∈ ( 𝐽 fClus { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ) ) )
57 34 56 mtod ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ¬ ∀ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 → ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) )
58 rexanali ⊢ ( ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ ¬ ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) ↔ ¬ ∀ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 → ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) )
59 rexnal ⊢ ( ∃ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ¬ ( 𝑢 ∩ 𝑛 ) ≠ ∅ ↔ ¬ ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ )
60 sseq2 ⊢ ( 𝑦 = 𝑛 → ( ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑛 ) )
61 60 elrab ⊢ ( 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ↔ ( 𝑛 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑛 ) )
62 sslin ⊢ ( ( 𝑋 ∖ 𝑥 ) ⊆ 𝑛 → ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ⊆ ( 𝑢 ∩ 𝑛 ) )
63 61 62 simplbiim ⊢ ( 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } → ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ⊆ ( 𝑢 ∩ 𝑛 ) )
64 ssn0 ⊢ ( ( ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ⊆ ( 𝑢 ∩ 𝑛 ) ∧ ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ ) → ( 𝑢 ∩ 𝑛 ) ≠ ∅ )
65 64 ex ⊢ ( ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ⊆ ( 𝑢 ∩ 𝑛 ) → ( ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ → ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) )
66 65 necon1bd ⊢ ( ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ⊆ ( 𝑢 ∩ 𝑛 ) → ( ¬ ( 𝑢 ∩ 𝑛 ) ≠ ∅ → ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅ ) )
67 inssdif0 ⊢ ( ( 𝑢 ∩ 𝑋 ) ⊆ 𝑥 ↔ ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅ )
68 66 67 syl6ibr ⊢ ( ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ⊆ ( 𝑢 ∩ 𝑛 ) → ( ¬ ( 𝑢 ∩ 𝑛 ) ≠ ∅ → ( 𝑢 ∩ 𝑋 ) ⊆ 𝑥 ) )
69 toponss ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐾 ) → 𝑢 ⊆ 𝑋 )
70 38 69 sylan ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → 𝑢 ⊆ 𝑋 )
71 df-ss ⊢ ( 𝑢 ⊆ 𝑋 ↔ ( 𝑢 ∩ 𝑋 ) = 𝑢 )
72 70 71 sylib ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑢 ∩ 𝑋 ) = 𝑢 )
73 72 sseq1d ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝑢 ∩ 𝑋 ) ⊆ 𝑥 ↔ 𝑢 ⊆ 𝑥 ) )
74 73 biimpd ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝑢 ∩ 𝑋 ) ⊆ 𝑥 → 𝑢 ⊆ 𝑥 ) )
75 68 74 syl9r ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝑢 ∩ ( 𝑋 ∖ 𝑥 ) ) ⊆ ( 𝑢 ∩ 𝑛 ) → ( ¬ ( 𝑢 ∩ 𝑛 ) ≠ ∅ → 𝑢 ⊆ 𝑥 ) ) )
76 63 75 syl5 ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } → ( ¬ ( 𝑢 ∩ 𝑛 ) ≠ ∅ → 𝑢 ⊆ 𝑥 ) ) )
77 76 rexlimdv ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ∃ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ¬ ( 𝑢 ∩ 𝑛 ) ≠ ∅ → 𝑢 ⊆ 𝑥 ) )
78 59 77 syl5bir ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ¬ ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ → 𝑢 ⊆ 𝑥 ) )
79 78 anim2d ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝑦 ∈ 𝑢 ∧ ¬ ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) → ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) )
80 79 reximdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ ¬ ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) )
81 58 80 syl5bir ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ( ¬ ∀ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 → ∀ 𝑛 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑦 } ( 𝑢 ∩ 𝑛 ) ≠ ∅ ) → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) )
82 57 81 mpd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) ) → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) )
83 82 anassrs ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ ( 𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) )
84 83 exp32 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ≠ 𝑋 → ( 𝑦 ∈ 𝑥 → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) ) )
85 29 84 pm2.61dne ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑦 ∈ 𝑥 → ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) )
86 85 ralrimiv ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) )
87 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝐾 ∈ Top )
88 eltop2 ⊢ ( 𝐾 ∈ Top → ( 𝑥 ∈ 𝐾 ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) )
89 14 87 88 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐾 ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ 𝐾 ( 𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥 ) ) )
90 86 89 mpbird ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐾 )
91 90 ex ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) → ( 𝑥 ∈ 𝐽 → 𝑥 ∈ 𝐾 ) )
92 91 ssrdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) → 𝐽 ⊆ 𝐾 )
93 13 92 impbida ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 ) ) )