Metamath Proof Explorer

Theorem fclsss2

Description: A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion fclsss2 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G → J fClus G ⊆ J fClus F

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → F ⊆ G
2 ssralv ⊢ F ⊆ G → ∀ s ∈ G x ∈ cls ⁡ J ⁡ s → ∀ s ∈ F x ∈ cls ⁡ J ⁡ s
3 1 2 syl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → ∀ s ∈ G x ∈ cls ⁡ J ⁡ s → ∀ s ∈ F x ∈ cls ⁡ J ⁡ s
4 simpl1 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → J ∈ TopOn ⁡ X
5 fclstopon ⊢ x ∈ J fClus G → J ∈ TopOn ⁡ X ↔ G ∈ Fil ⁡ X
6 5 adantl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → J ∈ TopOn ⁡ X ↔ G ∈ Fil ⁡ X
7 4 6 mpbid ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → G ∈ Fil ⁡ X
8 isfcls2 ⊢ J ∈ TopOn ⁡ X ∧ G ∈ Fil ⁡ X → x ∈ J fClus G ↔ ∀ s ∈ G x ∈ cls ⁡ J ⁡ s
9 4 7 8 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → x ∈ J fClus G ↔ ∀ s ∈ G x ∈ cls ⁡ J ⁡ s
10 simpl2 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → F ∈ Fil ⁡ X
11 isfcls2 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → x ∈ J fClus F ↔ ∀ s ∈ F x ∈ cls ⁡ J ⁡ s
12 4 10 11 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → x ∈ J fClus F ↔ ∀ s ∈ F x ∈ cls ⁡ J ⁡ s
13 3 9 12 3imtr4d ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G ∧ x ∈ J fClus G → x ∈ J fClus G → x ∈ J fClus F
14 13 ex ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G → x ∈ J fClus G → x ∈ J fClus G → x ∈ J fClus F
15 14 pm2.43d ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G → x ∈ J fClus G → x ∈ J fClus F
16 15 ssrdv ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ F ⊆ G → J fClus G ⊆ J fClus F