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	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ⇝𝑡 ‘ 𝐾 ) ⊆ ( ⇝𝑡 ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		idd	⊢ ( 𝐽 ⊆ 𝐾 → ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) → 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) )
2		idd	⊢ ( 𝐽 ⊆ 𝐾 → ( 𝑥 ∈ 𝑋 → 𝑥 ∈ 𝑋 ) )
3		ssralv	⊢ ( 𝐽 ⊆ 𝐾 → ( ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) → ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
4	1 2 3	3anim123d	⊢ ( 𝐽 ⊆ 𝐾 → ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) → ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ) )
5	4	ssopab2dv	⊢ ( 𝐽 ⊆ 𝐾 → { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } ⊆ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
6	5	3ad2ant3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } ⊆ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
7		lmfval	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → ( ⇝𝑡 ‘ 𝐾 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
8	7	3ad2ant2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ⇝𝑡 ‘ 𝐾 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
9		lmfval	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ⇝𝑡 ‘ 𝐽 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
10	9	3ad2ant1	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ⇝𝑡 ‘ 𝐽 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
11	6 8 10	3sstr4d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ⇝𝑡 ‘ 𝐾 ) ⊆ ( ⇝𝑡 ‘ 𝐽 ) )