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 𝐴 ) ⊆ 𝐹 )