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