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

Metamath Proof Explorer

Theorem trfilss

Description: If A is a member of the filter, then the filter truncated to A is a subset of the original filter. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion trfilss ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ⊆ 𝐹 )

Proof

Step Hyp Ref Expression
1 restval ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐹 ↦ ( 𝑥 ∩ 𝐴 ) ) )
2 filin ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝐹 )
3 2 3expa ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝐹 )
4 3 an32s ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝐹 )
5 4 fmpttd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 ↦ ( 𝑥 ∩ 𝐴 ) ) : 𝐹 ⟶ 𝐹 )
6 5 frnd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ran ( 𝑥 ∈ 𝐹 ↦ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝐹 )
7 1 6 eqsstrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( 𝐹 ↾t 𝐴 ) ⊆ 𝐹 )