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	|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) C_ F )

Proof

Step	Hyp	Ref	Expression
1		restval	|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) = ran ( x e. F |-> ( x i^i A ) ) )
2		filin	|- ( ( F e. ( Fil ` X ) /\ x e. F /\ A e. F ) -> ( x i^i A ) e. F )
3	2	3expa	|- ( ( ( F e. ( Fil ` X ) /\ x e. F ) /\ A e. F ) -> ( x i^i A ) e. F )
4	3	an32s	|- ( ( ( F e. ( Fil ` X ) /\ A e. F ) /\ x e. F ) -> ( x i^i A ) e. F )
5	4	fmpttd	|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( x e. F |-> ( x i^i A ) ) : F --> F )
6	5	frnd	|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ran ( x e. F |-> ( x i^i A ) ) C_ F )
7	1 6	eqsstrd	|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F |`t A ) C_ F )