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

Metamath Proof Explorer

Theorem sslm

Description: A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015)

		Ref	Expression
	Assertion	sslm	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to \underset{t}{⇝} (K) \subseteq \underset{t}{⇝} (J)$

Proof

Step	Hyp	Ref	Expression
1		idd	$⊢ J \subseteq K \to (f \in (X ↑_{𝑝𝑚} ℂ) \to f \in (X ↑_{𝑝𝑚} ℂ))$
2		idd	$⊢ J \subseteq K \to (x \in X \to x \in X)$
3		ssralv	$⊢ J \subseteq K \to (\forall u \in K (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u) \to \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))$
4	1 2 3	3anim123d	$⊢ J \subseteq K \to ((f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in K (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u)) \to (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u)))$
5	4	ssopab2dv	$⊢ J \subseteq K \to \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in K (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} \subseteq \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
6	5	3ad2ant3	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in K (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} \subseteq \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
7		lmfval	$⊢ K \in TopOn (X) \to \underset{t}{⇝} (K) = \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in K (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
8	7	3ad2ant2	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to \underset{t}{⇝} (K) = \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in K (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
9		lmfval	$⊢ J \in TopOn (X) \to \underset{t}{⇝} (J) = \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
10	9	3ad2ant1	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to \underset{t}{⇝} (J) = \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
11	6 8 10	3sstr4d	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to \underset{t}{⇝} (K) \subseteq \underset{t}{⇝} (J)$