Theorem flimss2

Description: A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

	Ref	Expression
Assertion	flimss2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐽 fLim 𝐺 ) ⊆ ( 𝐽 fLim 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	flimelbas	⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) → 𝑥 ∈ ∪ 𝐽 )
3	2	adantl	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑥 ∈ ∪ 𝐽 )
4		simpl1	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
6	4 5	syl	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑋 = ∪ 𝐽 )
7	3 6	eleqtrrd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑥 ∈ 𝑋 )
8		flimneiss	⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐺 )
9	8	adantl	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐺 )
10		simpl3	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝐺 ⊆ 𝐹 )
11	9 10	sstrd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 )
12		simpl2	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
13		elflim	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) ) )
14	4 12 13	syl2anc	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) ) )
15	7 11 14	mpbir2and	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
16	15	ex	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) )
17	16	ssrdv	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐽 fLim 𝐺 ) ⊆ ( 𝐽 fLim 𝐹 ) )