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 
|- ( ( 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 )